isBasis_sUnion — Mathlib

English

If Xs is a nonempty collection of sets, and I is a basis for every X in Xs, then I is a basis for the union of all X in Xs.

Русский

Если Xs — непустая коллекция множеств, и для каждого X из Xs I является базисом X, то I является базисом объединения всех X из Xs.

LaTeX

$$$ Xs.Nonempty \\rightarrow (\\forall X \\in Xs, M.IsBasis I X) \\rightarrow M.IsBasis I Xs.sUnion $$$

Lean4

theorem isBasis_sUnion {Xs : Set (Set α)} (hne : Xs.Nonempty) (h : ∀ X ∈ Xs, M.IsBasis I X) : M.IsBasis I (⋃₀ Xs) :=
  by
  rw [sUnion_eq_iUnion]
  have := Iff.mpr nonempty_coe_sort hne
  exact IsBasis.isBasis_iUnion _ fun X ↦ h X X.prop

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