mathlib3 documentation

data.nat.dist

Distance function on ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a simple distance function on naturals from truncated subtraction.

source
def nat.dist (n m : ℕ) :
ℕ

Distance (absolute value of difference) between natural numbers.

Equations
source
theorem nat.dist.def (n m : ℕ) :
n.dist m = n - m + (m - n)
source
theorem nat.dist_comm (n m : ℕ) :
n.dist m = m.dist n
source
@[simp]
theorem nat.dist_self (n : ℕ) :
n.dist n = 0
source
theorem nat.eq_of_dist_eq_zero {n m : ℕ} (h : n.dist m = 0) :
n = m
source
theorem nat.dist_eq_zero {n m : ℕ} (h : n = m) :
n.dist m = 0
source
theorem nat.dist_eq_sub_of_le {n m : ℕ} (h : n ≤ m) :
n.dist m = m - n
source
theorem nat.dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) :
n.dist m = n - m
source
theorem nat.dist_tri_left (n m : ℕ) :
m ≤ n.dist m + n
source
theorem nat.dist_tri_right (n m : ℕ) :
m ≤ n + n.dist m
source
theorem nat.dist_tri_left' (n m : ℕ) :
n ≤ n.dist m + m
source
theorem nat.dist_tri_right' (n m : ℕ) :
n ≤ m + n.dist m
source
theorem nat.dist_zero_right (n : ℕ) :
n.dist 0 = n
source
theorem nat.dist_zero_left (n : ℕ) :
0.dist n = n
source
theorem nat.dist_add_add_right (n k m : ℕ) :
(n + k).dist (m + k) = n.dist m
source
theorem nat.dist_add_add_left (k n m : ℕ) :
(k + n).dist (k + m) = n.dist m
source
theorem nat.dist_eq_intro {n m k l : ℕ} (h : n + m = k + l) :
n.dist k = l.dist m
source
theorem nat.dist.triangle_inequality (n m k : ℕ) :
n.dist k ≤ n.dist m + m.dist k
source
theorem nat.dist_mul_right (n k m : ℕ) :
(n * k).dist (m * k) = n.dist m * k
source
theorem nat.dist_mul_left (k n m : ℕ) :
(k * n).dist (k * m) = k * n.dist m
source
theorem nat.dist_succ_succ {i j : ℕ} :
i.succ.dist j.succ = i.dist j
source
theorem nat.dist_pos_of_ne {i j : ℕ} :
i ≠ j → 0 < i.dist j