English
If the family s is directed by inclusion and every s(i) is sSup independent, then the whole union ⋃ i s(i) is sSup independent.
Русский
Если семейство s упорядочено включением и каждый s(i) — sSup независим, то объединение ⋃i s(i) также является независимым.
LaTeX
$$$ sSupIndep (\bigcup_i s(i)) $$$
Lean4
theorem sSupIndep_iUnion_of_directed {η : Type*} {s : η → Set α} (hs : Directed (· ⊆ ·) s) (h : ∀ i, sSupIndep (s i)) :
sSupIndep (⋃ i, s i) := by
by_cases hη : Nonempty η
· rw [sSupIndep_iff_finite]
intro t ht
obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht
obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset
exact (h i).mono (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
· rintro a ⟨_, ⟨i, _⟩, _⟩
exfalso
exact hη ⟨i⟩
