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

@[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)