ground_not_isBase — Mathlib

English

If the dual of a matroid M has positive rank, then the ground set E of M is not a base of M.

Русский

Пусть у матроида M двойственный ранк положителен. Тогда множество грунта E не является базой M.

LaTeX

$$$ \operatorname{RankPos}(M^{\ast}) \Rightarrow \neg \bigl(M.IsBase(M.E)\bigr)$$$

Lean4

theorem ground_not_isBase (M : Matroid α) [h : RankPos M✶] : ¬M.IsBase M.E := by
  rwa [rankPos_iff, dual_isBase_iff, diff_empty] at h

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