empty

Mathlib.Combinatorics.Matroid.Rank.Finite

URI: https://scilib.ai/kg/mathlib#Matroid.IsRkFinite.empty

English

The empty set has finite rank in any matroid.

Русский

Пустое множество имеет конечный ранг в любом матроиде.

LaTeX

$$$M.IsRkFinite \emptyset$$$

Lean4

theorem empty (M : Matroid α) : M.IsRkFinite ∅ :=
  isRkFinite_of_finite M finite_empty

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

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

Разделы

Аффилиация

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