English
For any F ⊆ M.E, F is flat if and only if closure of F equals F.
Русский
Для любого F ⊆ M.E верно: F плоско тогда и только тогда, когда замыкание F равно F.
LaTeX
$$$M.IsFlat F \leftrightarrow M.closure F = F$$$
Lean4
theorem iInter {ι : Type*} [Nonempty ι] {Fs : ι → Set α} (hFs : ∀ i, M.IsFlat (Fs i)) : M.IsFlat (⋂ i, Fs i) :=
by
refine
⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_, (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩
obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans (iInter_subset _ i))
refine subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)
convert hIJ.isBasis_union (hIX.isBasis_union_of_subset hIJ.indep hJ) using 1
rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]
