insert

Mathlib.Combinatorics.Matroid.Rank.Finite

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

English

If X has finite rank in M, then X ∪ {e} has finite rank in M.

Русский

Если X имеет конечный ранг, то X ∪ {e} имеет конечный ранг.

LaTeX

$$$ M.IsRkFinite X \\rightarrow M.IsRkFinite (X \\cup \\{e\\}) $$$

Lean4

theorem insert (hX : M.IsRkFinite X) (e : α) : M.IsRkFinite (insert e X) :=
  by
  rw [← union_singleton]
  exact hX.union M.isRkFinite_singleton

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

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

Разделы

Аффилиация

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