isBasis_closure_right — Mathlib

English

If I is a basis for X in M in the primed sense, then I is a basis for the closure of X in M.

Русский

Если I является базисом X в M в обобщённом смысле IsBasis', то I является базисом замыкания X в M.

LaTeX

$$$\mathrm{Basis}'(I,X) \Rightarrow \mathrm{Basis}(I, \operatorname{cl}(X))$$$

Lean4

theorem isBasis_closure_right (h : M.IsBasis' I X) : M.IsBasis I (M.closure X) := by rw [← h.closure_eq_closure];
  exact h.indep.isBasis_closure

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