ne_imp_iff — Mathlib

English

For IsRefl r, x ≠ y → r x y iff r x y.

Русский

Для IsRefl r, при x ≠ y, верно r x y тогда и только тогда, что r x y.

LaTeX

$$$[IsRefl]\\alpha r) \\Rightarrow (x \\neq y \\Rightarrow r(x,y) \\Leftrightarrow r(x,y))$$$

Lean4

/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`. -/
theorem ne_imp_iff (h : Reflexive r) {x y : α} : x ≠ y → r x y ↔ r x y :=
  ⟨h.rel_of_ne_imp, fun hr _ ↦ hr⟩

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