Dissipate

The function dissipate takes s : α → Set β with LE α and returns ⋂ y ≤ x, s y. It is related to accumulate s := ⋃ y ≤ x, s y.

def Set.dissipate {α : Type u_1} {β : Type u_2} [LE α] (s : α → Set β) (x : α) : Set β

dissipate s is the intersection of s y for y ≤ x.

theorem Set.dissipate_def {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} : dissipate s x = ⋂ (y : α), ⋂ (_ : y ≤ x), s y

theorem Set.dissipate_eq_biInter_lt {β : Type u_2} {s : ℕ → Set β} {n : ℕ} : dissipate s n = ⋂ (k : ℕ), ⋂ (_ : k < n + 1), s k

@[simp]

theorem Set.mem_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y

theorem Set.dissipate_subset {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y

theorem Set.iInter_subset_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] (x : α) : ⋂ (i : α), s i ⊆ dissipate s x

theorem Set.antitone_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : Antitone (dissipate s)

theorem Set.dissipate_subset_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] {x y : α} (h : y ≤ x) : dissipate s x ⊆ dissipate s y

@[simp]

theorem Set.biInter_dissipate {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} {x : α} : ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y = dissipate s x

@[simp]

theorem Set.iInter_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : ⋂ (x : α), dissipate s x = ⋂ (x : α), s x

@[simp]

theorem Set.dissipate_bot {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] (s : α → Set β) : dissipate s ⊥ = s ⊥

@[simp]

theorem Set.dissipate_zero_nat {β : Type u_2} (s : ℕ → Set β) : dissipate s 0 = s 0

@[simp]

theorem Set.dissipate_succ {α : Type u_1} (s : ℕ → Set α) (n : ℕ) : dissipate s (n + 1) = dissipate s n ∩ s (n + 1)

theorem Set.exists_subset_dissipate_of_directed {α : Type u_1} {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s) (n : ℕ) : ∃ (m : ℕ), s m ⊆ dissipate s n

For a directed set of sets s : ℕ → Set α and n : ℕ, there exists m : ℕ (maybe larger than n) such that s m ⊆ dissipate s n.

theorem Set.directed_dissipate {α : Type u_1} {s : ℕ → Set α} : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) (dissipate s)

theorem Set.exists_dissipate_eq_empty_iff_of_directed {α : Type u_1} {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s) : (∃ (n : ℕ), dissipate s n = ∅) ↔ ∃ (n : ℕ), s n = ∅