disjoint_coloops

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsCircuit.disjoint_coloops

English

A circuit is disjoint from the set of coloops.

Русский

Цикл не пересекает множество колоопов.

LaTeX

$$$M.IsCircuit C \\rightarrow Disjoint\\left(C, M.coloops\\right)$$$

Lean4

theorem disjoint_coloops (hC : M.IsCircuit C) : Disjoint C M.coloops :=
  disjoint_right.2 <| fun _ he ↦ IsColoop.notMem_isCircuit he hC

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

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

Разделы

Аффилиация

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