eRank_eq_top_iff

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.eRank_eq_top_iff

English

The ENat-valued rank equals top if and only if the rank is infinite.

Русский

Ранг по ENat равен верхнему предельному значению тогда и только тогда, когда ранг бесконечен.

LaTeX

$$$M.eRank = ⊤ \\leftrightarrow M.RankInfinite$$$

Lean4

@[simp]
theorem eRank_eq_top_iff (M : Matroid α) : M.eRank = ⊤ ↔ M.RankInfinite := by
  rw [← not_rankFinite_iff, ← eRank_ne_top_iff, not_not]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru