isColoop_iff_diff_closure

Mathlib.Combinatorics.Matroid.Loop

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

English

A coloop e is equivalent to the statement that closure of E without e is not all of E.

Русский

Колооп e эквивалентно тому, что замыкание E без e не равно E.

LaTeX

$$$M.IsColoop e \\iff \\text{closure}(M.E \\setminus \\{e\\}) \\neq M.E$$$

Lean4

theorem isColoop_iff_diff_closure : M.IsColoop e ↔ M.closure (M.E \ { e }) ≠ M.E := by
  rw [isColoop_iff_diff_not_spanning, spanning_iff_closure_eq]

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

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

Разделы

Аффилиация

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