closure_eq_closure — Mathlib

English

For an independent I, closure I consists exactly of those x for which insert x into I yields a basis.

Русский

Для независимого I замыкание I равняется множеству тех x, для которых вставка x в I даёт базис.

LaTeX

$$$M.Indep I \\Rightarrow \\operatorname{cl}(I) = \\{x \\mid M.IsBasis I (\\operatorname{insert} x I)\\}$$$

Lean4

theorem closure_eq_closure (h : M.IsBasis I X) : M.closure I = M.closure X :=
  by
  refine subset_antisymm (M.closure_subset_closure h.subset) ?_
  rw [← M.closure_closure I, h.indep.closure_eq_setOf_isBasis_insert]
  exact M.closure_subset_closure fun e he ↦ (h.isBasis_subset (subset_insert _ _) (insert_subset he h.subset))

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