eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt

English

If two orderings x<y and y<x correspond to two other orderings x'<y' and y'<x' in the same way, then x=y iff x'=y'.

Русский

Если отношения x<y и y<x эквивалентно x'<y' и y'<x' одинаковым образом, тогда x=y эквивалентно x'=y'.

LaTeX

$$$ (x < y) \\leftrightarrow (x' < y') \\; \\Rightarrow \\; (y < x) \\leftrightarrow (y' < x') \\\\Rightarrow (x = y) \\iff (x' = y') $$$

Lean4

theorem eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt {x' y' : α} (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x')) :
    x = y ↔ x' = y' := by simp_rw [eq_iff_le_not_lt, ← not_lt, ltc, gtc]

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