pairwise_one_le_dist — Mathlib

English

For all m,n ∈ ℕ with m ≠ n, we have 1 ≤ dist(m,n). In other words, distinct natural numbers are at distance at least 1 apart.

Русский

Для любых m,n ∈ ℕ с m ≠ n выполнено 1 ≤ dist(m,n). Иными словами, разные натуральные числа разделены расстоянием не менее 1.

LaTeX

$$$\forall m,n \in \mathbb{N},\ m \neq n \implies 1 \le \operatorname{dist}(m,n)$$$

Lean4

theorem pairwise_one_le_dist : Pairwise fun m n : ℕ => 1 ≤ dist m n := fun _ _ hne =>
  Int.pairwise_one_le_dist <| mod_cast hne

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