Documentation

Mathlib.Data.Set.Dissipate

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.

source
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.

Equations
Instances For
    source
    theorem Set.dissipate_def {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} :
    dissipate s x = ⋂ (y : α), ⋂ (_ : y ≤ x), s y
    source
    theorem Set.dissipate_eq_biInter_lt {β : Type u_2} {s : ℕ → Set β} {n : ℕ} :
    dissipate s n = ⋂ (k : ℕ), ⋂ (_ : k < n + 1), s k
    source
    @[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
    source
    theorem Set.dissipate_subset {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x y : α} (hy : y ≤ x) :
    dissipate s x ⊆ s y
    source
    theorem Set.iInter_subset_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] (x : α) :
    ⋂ (i : α), s i ⊆ dissipate s x
    source
    theorem Set.antitone_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] :
    Antitone (dissipate s)
    source
    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
    source
    @[simp]
    theorem Set.biInter_dissipate {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} {x : α} :
    ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y = dissipate s x
    source
    @[simp]
    theorem Set.iInter_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] :
    ⋂ (x : α), dissipate s x = ⋂ (x : α), s x
    source
    @[simp]
    theorem Set.dissipate_bot {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] (s : α → Set β) :
    dissipate s ⊥ = s ⊥
    source
    @[simp]
    theorem Set.dissipate_zero_nat {β : Type u_2} (s : ℕ → Set β) :
    dissipate s 0 = s 0
    source
    @[simp]
    theorem Set.dissipate_succ {α : Type u_1} (s : ℕ → Set α) (n : ℕ) :
    dissipate s (n + 1) = dissipate s n ∩ s (n + 1)
    source
    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.

    source
    theorem Set.directed_dissipate {α : Type u_1} {s : ℕ → Set α} :
    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) (dissipate s)
    source
    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 = ∅