delete_rankFinite

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

If M has finite rank, then the deletion M \ D also has finite rank.

Русский

Если ранг M конечен, то ранг M \ D также конечен.

LaTeX

$$$ [M.RankFinite] \Rightarrow (M \setminus D).RankFinite $$$

Lean4

instance delete_rankFinite [RankFinite M] : RankFinite (M ＼ D) :=
  restrict_rankFinite _

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

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

Разделы

Аффилиация

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