English
For any α, X, Y, the closure of the union of closures equals the closure of the union.
Русский
Для любых α, X, Y: cl(cl(X) ∪ cl(Y)) = cl(X ∪ Y).
LaTeX
$$$\\operatorname{cl}(\\operatorname{cl}(X) \\cup \\operatorname{cl}(Y)) = \\operatorname{cl}(X \\cup Y)$$$
Lean4
theorem closure_eq_setOf_isBasis_insert (hI : M.Indep I) : M.closure I = {x | M.IsBasis I (insert x I)} :=
by
set F := {x | M.IsBasis I (insert x I)}
have hIF : M.IsBasis I F := hI.isBasis_setOf_insert_isBasis
have hF : M.IsFlat F :=
by
refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩
exact
(hIF.isBasis_of_isBasis_of_subset_of_subset (hJX.isBasis_union hJF) hJF.subset
(hIF.subset.trans subset_union_right)).isBasis_subset
(subset_insert _ _) (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))
rw [subset_antisymm_iff, closure_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]
· rintro F' ⟨hF', hIF'⟩ e (he : M.IsBasis I (insert e I))
rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'
obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset hIF' hF'.2
exact (hF'.1 hJ (he.isBasis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))
exact ⟨hF, inter_subset_left.trans hIF.subset⟩
