removeLoops_idem

Mathlib.Combinatorics.Matroid.Loop

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

English

Removing loops twice yields the same matroid as removing loops once.

Русский

Удаление петель дважды даёт тот же матроид, что и одно удаление.

LaTeX

$$$\operatorname{removeLoops}(\operatorname{removeLoops}(M)) = \operatorname{removeLoops}(M)$$$

Lean4

theorem removeLoops_idem (M : Matroid α) : M.removeLoops.removeLoops = M.removeLoops := by simp

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

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

Разделы

Аффилиация

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