dual_isLoop_iff_isColoop — Mathlib

English

An element is a Loop in the dual if and only if it is a Coloop in the original.

Русский

Элемент является петлей двойственного, если и только если он колооп в исходном матроидe.

LaTeX

$$M✶.IsLoop e \leftrightarrow M.IsColoop e$$

Lean4

@[simp]
theorem dual_isLoop_iff_isColoop : M✶.IsLoop e ↔ M.IsColoop e :=
  ⟨fun h ↦ by rw [← dual_dual M]; exact h.dual_isColoop, IsColoop.dual_isLoop⟩

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