delete_finite

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

If M is finite, then M \ D is finite.

Русский

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

LaTeX

$$$ (M \setminus D).Finite $$$

Lean4

instance delete_finite [M.Finite] : (M ＼ D).Finite :=
  ⟨M.ground_finite.diff⟩

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

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

Разделы

Аффилиация

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