compl_loops_eq

Mathlib.Combinatorics.Matroid.Loop

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

English

The ground minus loops equals the set of nonloops.

Русский

Ground minus петли равен множеству не-петель.

LaTeX

$$$ M.E \ M.loops = \{ e \mid M.IsNonloop e \} $$$

Lean4

theorem compl_loops_eq (M : Matroid α) : M.E \ M.loops = {e | M.IsNonloop e} := by
  simp [Set.ext_iff, isNonloop_iff, and_comm, isLoop_iff]

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

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

Разделы

Аффилиация

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