pairwise_one_le_dist — Mathlib

English

For any distinct integers m,n, we have 1 ≤ dist m n; in particular, the distance between distinct integers is at least 1.

Русский

Для любых различных целых m,n выполняется 1 ≤ dist m n; расстояние между различными целыми не менее 1.

LaTeX

$$Pairwise (\\lambda m n, 1 \\le dist m n)$$

Lean4

theorem pairwise_one_le_dist : Pairwise fun m n : ℤ => 1 ≤ dist m n :=
  by
  intro m n hne
  rw [dist_eq]; norm_cast; rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

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