exists_of_eRank_eq_zero — Mathlib

English

If the eRank of a matroid M is zero, then M is loopyOn some subset X; in particular, M = loopyOn(M.E), i.e., every element is a loop.

Русский

Если eRank матроида M равен нулю, то существует подмножество X такое, что M = loopyOn(X); в частности, M = loopyOn(M.E), то есть каждый элемент является петлёй.

LaTeX

$$$ eRank(M) = 0 \\rightarrow \\exists X, M = loopyOn(X)$$$

Lean4

theorem exists_of_eRank_eq_zero (h : M.eRank = 0) : ∃ X, M = loopyOn X :=
  ⟨M.E, by simpa [eRank_eq_zero_iff] using h⟩

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