loops_eq_empty

Mathlib.Combinatorics.Matroid.Loop

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

English

If a matroid M is loopless, then its set of loops is empty: M.loops = ∅.

Русский

Если матроид M не содержит петель, то множество петель пусто: M.loops = ∅.

LaTeX

$$$$ M.Loopless \Rightarrow M.loops = \emptyset. $$$$

Lean4

@[simp]
theorem loops_eq_empty (M : Matroid α) [Loopless M] : M.loops = ∅ :=
  ‹Loopless M›.loops_eq_empty

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

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

Разделы

Аффилиация

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