loopless_iff_forall_isNonloop — Mathlib

English

A matroid M is loopless iff every element of its ground set is a nonloop.

Русский

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

LaTeX

$$$$ M.Loopless \iff \forall e \in M.E, M.IsNonloop(e). $$$$

Lean4

theorem loopless_iff_forall_isNonloop : M.Loopless ↔ ∀ e ∈ M.E, M.IsNonloop e :=
  ⟨fun _ _ he ↦ isNonloop_of_loopless he, fun h ↦
    ⟨subset_empty_iff.1 (fun e (he : M.IsLoop e) ↦ (h e he.mem_ground).not_isLoop he)⟩⟩

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