removeLoops_loopless

Mathlib.Combinatorics.Matroid.Loop

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

English

The matroid M.removeLoops is loopless.

Русский

Матроид M.removeLoops без петель.

LaTeX

$$$$ \text{Loopless}(M.removeLoops). $$$$

Lean4

instance removeLoops_loopless (M : Matroid α) : Loopless M.removeLoops := by
  simp [loopless_iff_forall_isNonloop, removeLoops]

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

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

Разделы

Аффилиация

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