eq_of_closure_subset — Mathlib

English

If I is a basis of X, and J ⊆ I, and X ⊆ closure(J), then J = I.

Русский

Если I является базисом X, J ⊆ I, и X ⊆ closure(J), тогда J = I.

LaTeX

$$$M.IsBasis I X \\rightarrow J \\subseteq I \\rightarrow X \\subseteq M.closure J \\rightarrow J = I$$$

Lean4

theorem eq_of_closure_subset (hI : M.IsBasis I X) (hJI : J ⊆ I) (hJ : X ⊆ M.closure J) : J = I :=
  by
  rw [← hI.indep.closure_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]
  exact hI.subset.trans hJ

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