one_le_eRank — Mathlib

English

If the matroid M has a positive rank (RankPos), then 1 ≤ eRank(M). In particular, the extended rank is at least 1 for any matroid with nonempty rank.

Русский

Если у матроидa M положительная ранговая характеристика (RankPos), то 1 ≤ eRank(M). В частности, расширенный ранг не меньше единицы для любого матриода с непустым рангом.

LaTeX

$$$ 1 \\le M.eRank $$$

Lean4

theorem one_le_eRank (M : Matroid α) [RankPos M] : 1 ≤ M.eRank :=
  by
  obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, one_le_encard_iff_nonempty]
  exact hB.nonempty

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