insert_isBasis_insert — Mathlib

English

If I is a basis for X, then inserting e into I yields a basis for I ∪ {e} if and only if either I ∪ {e} is dependent or e ∈ I.

Русский

Если I является базисом X, то добавление элемента e в I образует базис I ∪ {e} тогда и только тогда, когда либо I ∪ {e} зависимо, либо e ∈ I.

LaTeX

$$$ M.IsBasis I X \\rightarrow M.Indep (I) \\rightarrow M.IsBasis I (I \\cup \\{e\\}) \\iff M.Dep(I \\cup \\{e\\}) \\lor e \\in I $$$

Lean4

theorem insert_isBasis_insert (hI : M.IsBasis I X) (h : M.Indep (insert e I)) : M.IsBasis (insert e I) (insert e X) :=
  by
  simp_rw [← union_singleton] at *
  exact hI.union_isBasis_union (h.subset subset_union_right).isBasis_self h

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