singleton_isCocircuit — Mathlib

English

Let M be a matroid on a ground set. Then the singleton {e} is a cocircuit of M if and only if e is a coloop of M.

Русский

Пусть M — матроид на множествах; множество {e} является кококритом M тогда и только тогда, когда e является колоопом M.

LaTeX

$$$M.IsCocircuit\\left\\{e\\}\\right\\) \\iff M.IsColoop\\ left(e\\right)$$$

Lean4

theorem singleton_isCocircuit : M.IsCocircuit { e } ↔ M.IsColoop e := by simp

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