ssubset_ground — Mathlib

English

If M has RankPos in its dual and B is a base of M, then B is a proper subset of the ground E.

Русский

Если у M двойственный матроид имеет положительный ранг и B является базой M, то B является proper-подмножеством грунта E.

LaTeX

$$$ \operatorname{RankPos}(M^{\ast}) \wedge M.IsBase(B) \Rightarrow B \subsetneq M.E$$$

Lean4

theorem ssubset_ground [h : RankPos M✶] (hB : M.IsBase B) : B ⊂ M.E :=
  hB.subset_ground.ssubset_of_ne (by rintro rfl; exact M.ground_not_isBase hB)

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