eRank_eq_zero_iff — Mathlib

English

eRank equals zero iff the matroid is loopy on its ground: eRank = 0 ↔ M = loopyOn M.E.

Русский

eRank = 0 тогда и только тогда, когда матроид лоупи на своей области определения: eRank = 0 ↔ M = loopyOn M.E.

LaTeX

$$M.eRank = 0 ↔ M = loopyOn M.E$$

Lean4

theorem eRank_eq_zero_iff : M.eRank = 0 ↔ M = loopyOn M.E :=
  by
  refine ⟨fun h ↦ closure_empty_eq_ground_iff.1 ?_, fun h ↦ by rw [h, eRank_loopyOn]⟩
  obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, encard_eq_zero] at h
  rw [← h, hB.closure_eq]

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