isNonloop_iff_mem_compl_loops

Mathlib.Combinatorics.Matroid.Loop

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

English

An element is a nonloop iff it lies in the ground set minus loops.

Русский

Элемент является не-петлей тогда и только тогда, когда он принадлежит ground \ M.loops.

LaTeX

$$$ M.IsNonloop e \iff e \in M.E \setminus M.loops $$$

Lean4

theorem isNonloop_iff_mem_compl_loops : M.IsNonloop e ↔ e ∈ M.E \ M.loops := by
  rw [isNonloop_iff, IsLoop, and_comm, mem_diff]

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

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

Разделы

Аффилиация

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