isColoop_iff_diff_not_spanning

Mathlib.Combinatorics.Matroid.Loop

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

English

A coloop e is equivalent to the statement that M.E minus e does not span the ground set.

Русский

Колооп e эквивалентен утверждению, что M.E без e не порождает все множество.

LaTeX

$$$M.IsColoop e \\iff \\neg M.Spanning (M.E \\setminus \\{e\\})$$$

Lean4

theorem isColoop_iff_diff_not_spanning : M.IsColoop e ↔ ¬M.Spanning (M.E \ { e }) :=
  (M.isColoop_tfae e).out 0 6

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

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

Разделы

Аффилиация

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