setOf_isNonloop_eq

Mathlib.Combinatorics.Matroid.Loop

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

English

The set {e | M.IsNonloop e} equals M.E \ M.loops.

Русский

Множество {e | M.IsNonloop e} равно M.E \ M.loops.

LaTeX

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

Lean4

theorem setOf_isNonloop_eq (M : Matroid α) : {e | M.IsNonloop e} = M.E \ M.loops :=
  Set.ext (fun _ ↦ isNonloop_iff_mem_compl_loops)

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

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

Разделы

Аффилиация

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