delete_loops_eq

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

Deleting all loops yields the same as removing loops from the matroid.

Русский

Удаление всех петель дает тот же матроид, что и удаление петель из него.

LaTeX

$$$ (M \ D).loops = M.loops \ D $$$

Lean4

@[simp]
theorem delete_loops_eq (M : Matroid α) (D : Set α) : (M ＼ D).loops = M.loops \ D := by simp [loops]

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

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

Разделы

Аффилиация

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