isColoop_iff_forall_mem_closure_iff_mem

English

For any matroid M and any X, the intersection of closure(X) with the coloops equals X ∩ coloops.

Русский

Для любого матроидa M и множества X, замыкание(X) пересекает множества колоопов так же, как и X пересечении с колоопами.

LaTeX

$$$M.closure X \\cap M.coloops = X \\cap M.coloops$$$

Lean4

theorem isColoop_iff_forall_mem_closure_iff_mem : M.IsColoop e ↔ (∀ X, e ∈ M.closure X ↔ e ∈ X) :=
  (M.isColoop_tfae e).out 0 5

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