delete_eq_restrict

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

The deletion M \ D is exactly the restriction M ↾ (M.E \ D).

Русский

Удаление M \ D равно ограничению M на M.E \ D.

LaTeX

$$M \ D = M ↾ (M.E \ D)$$

Lean4

theorem delete_eq_restrict (M : Matroid α) (D : Set α) : M ＼ D = M ↾ (M.E \ D) :=
  rfl

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

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

Разделы

Аффилиация

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