not_isLoop

Mathlib.Combinatorics.Matroid.Loop

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

English

For a loopless matroid M and any element e, not e is a loop: not M.IsLoop(e).

Русский

Для матроидa M без петель и любого элемента e, e не является петлей: не M.IsLoop(e).

LaTeX

$$$$ \forall e, \neg M.IsLoop(e). $$$$

Lean4

theorem not_isLoop (M : Matroid α) [Loopless M] (e : α) : ¬M.IsLoop e := fun h ↦
  (isNonloop_of_loopless (e := e)).not_isLoop h

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

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

Разделы

Аффилиация

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