not_isColoop

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsLoop.not_isColoop

← MathLib Explorer

English

A loop cannot be a coloop: if e is a loop, then e is not a coloop.

Русский

Петля не может быть колоопом: если e петля, то e не колооп.

LaTeX

$$$M.IsLoop e \\rightarrow \\lnot M.IsColoop e$$$

Lean4

theorem not_isColoop (h : M.IsLoop e) : ¬M.IsColoop e :=
  by
  rw [← dual_isLoop_iff_isColoop]; rw [← dual_dual M, dual_isLoop_iff_isColoop] at h
  exact h.isNonloop.not_isLoop

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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