isBasis_union_of_subset — Mathlib

English

If I is a basis of X and J is independent with I ⊆ J, then J ∪ X has a basis extending J.

Русский

Если I является базисом X и J независим с I ⊆ J, то J ∪ X имеет базис, включающий J.

LaTeX

$$$ M.IsBasis I X \\land J \\supseteq I \\land M.Indep J \\rightarrow M.IsBasis J (J \\cup X) $$$

Lean4

theorem isBasis_union_of_subset (hI : M.IsBasis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) : M.IsBasis J (J ∪ X) :=
  by
  convert hJ.isBasis_self.union_isBasis_union hI _ <;> rw [union_eq_self_of_subset_right hIJ]
  assumption

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