not_rankInfinite_iff

Mathlib.Combinatorics.Matroid.Basic

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

English

For bases B1, B2, the finiteness of B1 \ B2 equals the finiteness of B2 \ B1.

Русский

Для баз B1, B2 конечность B1 \ B2 эквивалентна конечности B2 \ B1.

LaTeX

$$(hB1 : M.IsBase B1) → (hB2 : M.IsBase B2) → (B1 \ B2).Finite ↔ (B2 \ B1).Finite$$

Lean4

@[simp]
theorem not_rankInfinite_iff (M : Matroid α) : ¬RankInfinite M ↔ RankFinite M := by rw [← not_rankFinite_iff, not_not]

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

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

Разделы

Аффилиация

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