reflexive_ne_imp_iff — Mathlib

English

If IsRefl α r is given, then x ≠ y → r x y ↔ 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`. Unlike `Reflexive.ne_imp_iff`, this uses `[IsRefl α r]`. -/
theorem reflexive_ne_imp_iff [IsRefl α r] {x y : α} : x ≠ y → r x y ↔ r x y :=
  IsRefl.reflexive.ne_imp_iff

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