Saturation

def Set.Saturates {ι : Type u_1} {α : Type u_2} (f : ι → Set α) (s : Set α) : Prop

f : ι → Set α saturates s : Set α iff f i is a subset of s whenever f i and s has any intersection at all.

Equations

• Set.Saturates f s = ∀ (i : ι), (f i ∩ s).Nonempty → f i ⊆ s

@[simp]

theorem Set.saturates_compl {ι : Type u_1} {α : Type u_2} {f : ι → Set α} {s : Set α} (hs : Saturates f s) : Saturates f sᶜ

If f saturates s, then f saturates its complement sᶜ as well.

theorem Set.saturates_eq_biUnion {ι : Type u_1} {α : Type u_2} {f : ι → Set α} {s : Set α} (hs : Saturates f s) (hc : ⋃ (i : ι), f i = univ) : s = ⋃ i ∈ {i : ι | (f i ∩ s).Nonempty}, f i

If f is a cover and saturates s, then s is the union of all f i that intersects s.