loops_subset_ground — Mathlib

English

The loops of a matroid are precisely the elements that are always contained in any dependent set.

Русский

Петелью матроида является элемент, который всегда принадлежит любому зависимому множеству.

LaTeX

$$$\\text{loops}(M) = M.closure(\\emptyset)\\quad\\text{and}\\quad M.loops = M.closure(\\emptyset)$$$

Lean4

@[aesop unsafe 20% (rule_sets := [Matroid])]
theorem loops_subset_ground (M : Matroid α) : M.loops ⊆ M.E :=
  M.closure_subset_ground ∅

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