fromRel_irreflexive — Mathlib

English

Irreflexive r is equivalent to: for all z in fromRel sym, z is not diagonal.

Русский

Необратимая (иррефлексивная) связь r эквивалентна тому, что для любого z ∈ fromRel sym z не диагонален.

LaTeX

$$$$ \Irreflexive r \iff \forall \{z\}, z \in \mathrm{fromRel}(sym) \to \lnot \IsDiag(z). $$$$

Lean4

theorem fromRel_irreflexive {sym : Symmetric r} : Irreflexive r ↔ ∀ {z}, z ∈ fromRel sym → ¬IsDiag z :=
  { mp := by intro h; apply Sym2.ind; aesop
    mpr := fun h _ hr => h (fromRel_prop.mpr hr) rfl }

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