eq_loopyOn_or_rankPos — Mathlib

English

Let M be a Matroid on α with ground set E. Then either M equals loopyOn E or RankPos M holds.

Русский

Пусть M — матроид над множеством α с опорным множеством E. Тогда либо M равно loopyOn E, либо выполняется RankPos(M).

LaTeX

$$$ M = \operatorname{loopyOn}(M.E) \lor \operatorname{RankPos}(M) $$$

Lean4

theorem eq_loopyOn_or_rankPos (M : Matroid α) : M = loopyOn M.E ∨ RankPos M := by rw [← empty_isBase_iff, rankPos_iff];
  apply em

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