closure_inter_eq_self_of_subset — Mathlib

English

If I ⊆ X and I independent, then cl(I) ∩ X = I.

Русский

Если I ⊆ X и I независим, то cl(I) ∩ X = I.

LaTeX

$$$J \subseteq I \land \mathrm{Indep}(I) \Rightarrow \operatorname{cl}(J) \cap I = J$$$

Lean4

theorem closure_inter_eq_self_of_subset (hI : M.Indep I) (hJI : J ⊆ I) : M.closure J ∩ I = J :=
  by
  have hJ := hI.subset hJI
  rw [subset_antisymm_iff, and_iff_left (subset_inter (M.subset_closure _) hJI)]
  rintro e ⟨heJ, heI⟩
  exact hJ.isBasis_closure.mem_of_insert_indep heJ (hI.subset (insert_subset heI hJI))

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