rel_of_ne_imp — Mathlib

English

If r is reflexive and x ≠ y implies r x y, then r x y holds.

Русский

Если r рефлексивно и при x ≠ y следует r x y, тогда r x y выполняется.

LaTeX

$$$\\text{If } h:\\text{Reflexive } r \\text{ and } hr : x \\neq y \\Rightarrow r(x,y), \\text{ then } r(x,y)$$$

Lean4

/-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
it suffices to show it holds when `x ≠ y`. -/
theorem rel_of_ne_imp (h : Reflexive r) {x y : α} (hr : x ≠ y → r x y) : r x y := by grind [Reflexive]

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