isColoop_iff_forall_mem_isBase — Mathlib

English

A matroid element e is a coloop if and only if e lies in every base of the matroid.

Русский

Элемент e матроидa является колоопом тогда и только тогда, когда он принадлежит каждому базису матроидa.

LaTeX

$$$M.IsColoop e \\iff \\forall B\\, (M.IsBase B \\to e \\in B)$$$

Lean4

theorem isColoop_iff_forall_mem_isBase : M.IsColoop e ↔ ∀ ⦃B⦄, M.IsBase B → e ∈ B :=
  (M.isColoop_tfae e).out 0 3

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