loopless_iff_forall_not_isLoop — Mathlib

English

A matroid M is loopless iff every circuit is nontrivial.

Русский

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

LaTeX

$$$$ M.Loopless \iff \forall C, M.IsCircuit(C) \rightarrow C.Nontrivial. $$$$

Lean4

theorem loopless_iff_forall_not_isLoop : M.Loopless ↔ ∀ e ∈ M.E, ¬M.IsLoop e :=
  ⟨fun _ e _ ↦ M.not_isLoop e, fun h ↦ loopless_iff_forall_isNonloop.2 fun e he ↦ (not_isLoop_iff he).1 (h e he)⟩

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