removeLoops_isNonloop

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsNonloop.removeLoops_isNonloop

English

If e is nonloop in M, then e remains nonloop in M.removeLoops.

Русский

Если e не петля в M, то e остаётся не петлёй в M.removeLoops.

LaTeX

$$(\forall e)\; M.IsNonloop(e) \Rightarrow M.removeLoops.IsNonloop(e)$$

Lean4

theorem removeLoops_isNonloop (he : M.IsNonloop e) : M.removeLoops.IsNonloop e := by simpa

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

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

Разделы

Аффилиация

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