delete_finitary

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

If M is finitely generated (Finitary), then M \ D is also finitely generated.

Русский

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

LaTeX

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

Lean4

instance delete_finitary (M : Matroid α) [Finitary M] (D : Set α) : Finitary (M ＼ D) :=
  inferInstanceAs <| Finitary (M ↾ (M.E \ D))

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

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

Разделы

Аффилиация

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