isRkFinite_ground

Mathlib.Combinatorics.Matroid.Rank.Finite

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

English

If M has RankFinite, then M.IsRkFinite M.E holds.

Русский

Если у M конечный ранг, то выполняется M.IsRkFinite M.E.

LaTeX

$$$[RankFinite M] \\Rightarrow M.IsRkFinite M.E$$$

Lean4

theorem isRkFinite_ground (M : Matroid α) [RankFinite M] : M.IsRkFinite M.E := by rwa [isRkFinite_ground_iff_rankFinite]

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

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

Разделы

Аффилиация

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