delete_ground

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

Let M be a matroid and D ⊆ E(M). The ground of the deleted matroid equals the ground of M minus D; i.e., (M \\ D).E = M.E \\ D.

Русский

Пусть M — матроид и D ⊆ E(M).GROUND удаленного матройда равен E(M) \setminus D; то есть (M \\ D).E = M.E \\ D.

LaTeX

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

Lean4

@[simp]
theorem delete_ground (M : Matroid α) (D : Set α) : (M ＼ D).E = M.E \ D :=
  rfl

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

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

Разделы

Аффилиация

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