mem_fromRel_irrefl_other_ne — Mathlib

English

If r is irreflexive and z ∈ fromRel sym with a ∈ z, then the other element is not equal to a.

Русский

Если r иррефлексивно и z ∈ fromRel sym и a ∈ z, то другой элемент не равен a.

LaTeX

$$$$ \text{If } \text{irrefl} : \mathrm{Irreflexive}(r) \text{ and } z \in \mathrm{fromRel}(sym) \text{ and } a \in z, \; \mathrm{Mem.other}(a) \neq a. $$$$

Lean4

theorem mem_fromRel_irrefl_other_ne {sym : Symmetric r} (irrefl : Irreflexive r) {a : α} {z : Sym2 α}
    (hz : z ∈ fromRel sym) (h : a ∈ z) : Mem.other h ≠ a :=
  other_ne (fromRel_irreflexive.mp irrefl hz) h

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