eq_of_spanning_subset — Mathlib

English

If B is a base and X ⊆ B with X spanning in its own right, then B = X (i.e., a spanning set contained in a base must equal the base).

Русский

Если B — база, а X ⊆ B и X порождает всю систему, то B = X.

LaTeX

$$$$ (M.IsBase B) \rightarrow (M.Spanning X) \land (X \subseteq B) \rightarrow B = X. $$$$

Lean4

theorem eq_of_spanning_subset (hI : M.Indep I) (hS : M.Spanning S) (hSI : S ⊆ I) : S = I :=
  ((hI.subset hSI).isBase_of_spanning hS).eq_of_subset_indep hI hSI

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