closure_inter_isBasis_closure — Mathlib

English

If X ∩ I is a basis of X and I is independent, then closure X is contained in closure I and related inclusions hold; the closed sets expand compatibly.

Русский

Если X ∩ I является базисом X и I независимо, то замыкание X относится к замыканию I и выполняются соответствующие включения.

LaTeX

$$$\forall h:\ M.IsBasis (X \cap I) X,\ M.Indep I \Rightarrow M.IsBasis (M.closure X \cap I) (M.closure X)$$$

Lean4

theorem closure_inter_isBasis_closure (h : M.IsBasis (X ∩ I) X) (hI : M.Indep I) :
    M.IsBasis (M.closure X ∩ I) (M.closure X) :=
  by
  rw [hI.inter_isBasis_closure_iff_subset_closure_inter] at h ⊢
  exact
    (M.closure_subset_closure_of_subset_closure h).trans
      (M.closure_subset_closure (inter_subset_inter_left _ (h.trans (M.closure_subset_closure inter_subset_left))))

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