ssubset_ground — Mathlib

English

Every independent set I in a matroid with RankPos in the dual is strictly contained in the ground E.

Русский

Каждое независимое множество I в матроидe с RankPos двойственного ранга строго содержится в грунте E.

LaTeX

$$$ \operatorname{RankPos}(M^{\ast}) \to (M.Indep(I) \Rightarrow I \subsetneq M.E)$$$

Lean4

theorem ssubset_ground [h : RankPos M✶] (hI : M.Indep I) : I ⊂ M.E := by obtain ⟨B, hB⟩ := hI.exists_isBase_superset;
  exact hB.2.trans_ssubset hB.1.ssubset_ground

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