isBase_of_isBasis_superset — Mathlib

English

If B is a base and B ⊆ X, and I is a basis of X, then I is a base.

Русский

Если B является базисом и B ⊆ X, и I является базисом X, тогда I является базисом.

LaTeX

$$$ M.IsBase B \\rightarrow B \\subseteq X \\rightarrow M.IsBasis I X \\rightarrow M.IsBase I $$$

Lean4

theorem isBase_of_isBasis_superset (hB : M.IsBase B) (hBX : B ⊆ X) (hIX : M.IsBasis I X) : M.IsBase I :=
  by
  by_contra h
  obtain ⟨e, heBI, he⟩ := hIX.indep.exists_insert_of_not_isBase h hB
  exact heBI.2 (hIX.mem_of_insert_indep (hBX heBI.1) he)

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