eRk_ne_top_iff

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

eRk X is not top if and only if X is finite-rank.

Русский

eRk X не равно верхнему пределу тогда и только тогда, когда ранг X конечен.

LaTeX

$$$M.eRk X \\neq ⊤ \\leftrightarrow M.IsRkFinite X$$$

Lean4

theorem eRk_ne_top_iff : M.eRk X ≠ ⊤ ↔ M.IsRkFinite X := by simp

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

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

Разделы

Аффилиация

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