rankInfinite_iff_aleph0_le_cRank

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

English

RankInfinite is equivalent to aleph0 ≤ cRank.

Русский

RankInfinite эквивалентно ℵ₀ ≤ cRank.

LaTeX

$$RankInfinite ⇔ ℵ₀ ≤ cRank$$

Lean4

theorem rankInfinite_iff_aleph0_le_cRank : M.RankInfinite ↔ ℵ₀ ≤ M.cRank := by
  rw [← not_lt, ← rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff]

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

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

Разделы

Аффилиация

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