freeOn_not_isLoop

Mathlib.Combinatorics.Matroid.Loop

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

English

In the free matroid on E, no element is a loop.

Русский

В свободном матроиде на E ни один элемент не является петлей.

LaTeX

$$$ \forall E, \forall e, \neg (freeOn E).IsLoop e $$$

Lean4

@[simp]
theorem freeOn_not_isLoop (E : Set α) (e : α) : ¬(freeOn E).IsLoop e := by simp [isLoop_iff, loops]

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

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

Разделы

Аффилиация

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