isRkFinite_ground_iff_rankFinite

Mathlib.Combinatorics.Matroid.Rank.Finite

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

English

The simp lemma states the same equivalence as isRkFinite_ground_iff_rankFinite.

Русский

Лемма для упрощения сообщает то же эквивалентность, что и isRkFinite_ground_iff_rankFinite.

LaTeX

$$$Eq\\,(M.IsRkFinite M.E)\\, M.RankFinite$$$

Lean4

@[simp]
theorem isRkFinite_ground_iff_rankFinite : M.IsRkFinite M.E ↔ M.RankFinite := by
  rw [IsRkFinite, restrict_ground_eq_self]

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

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

Разделы

Аффилиация

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