iSupIndep_sUnion_of_directed — Mathlib

English

If a family of sets s is directed by inclusion and each a ∈ s has sSupIndep, then sSupIndep of the union ⋃ s is preserved.

Русский

Если семейство множеств s направлено включением и каждый элемент множества удовлетворяет sSupIndep, то независимость сохраняется для объединения.

LaTeX

$$$ sSupIndep (⋃_0 s) $$$

Lean4

theorem iSupIndep_sUnion_of_directed {s : Set (Set α)} (hs : DirectedOn (· ⊆ ·) s) (h : ∀ a ∈ s, sSupIndep a) :
    sSupIndep (⋃₀ s) := by
  rw [Set.sUnion_eq_iUnion]
  exact sSupIndep_iUnion_of_directed hs.directed_val (by simpa using h)

Похожие утверждения