# Documentation

Mathlib.Data.Nat.Dist

# Distance function on ℕ #

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

def Nat.dist (n : ) (m : ) :

Distance (absolute value of difference) between natural numbers.

Equations
theorem Nat.dist.def (n : ) (m : ) :
Nat.dist n m = n - m + (m - n)
theorem Nat.dist_comm (n : ) (m : ) :
@[simp]
theorem Nat.dist_self (n : ) :
Nat.dist n n = 0
theorem Nat.eq_of_dist_eq_zero {n : } {m : } (h : Nat.dist n m = 0) :
n = m
theorem Nat.dist_eq_zero {n : } {m : } (h : n = m) :
Nat.dist n m = 0
theorem Nat.dist_eq_sub_of_le {n : } {m : } (h : n m) :
Nat.dist n m = m - n
theorem Nat.dist_eq_sub_of_le_right {n : } {m : } (h : m n) :
Nat.dist n m = n - m
theorem Nat.dist_tri_left (n : ) (m : ) :
m Nat.dist n m + n
theorem Nat.dist_tri_right (n : ) (m : ) :
m n + Nat.dist n m
theorem Nat.dist_tri_left' (n : ) (m : ) :
n Nat.dist n m + m
theorem Nat.dist_tri_right' (n : ) (m : ) :
n m + Nat.dist n m
theorem Nat.dist_add_add_right (n : ) (k : ) (m : ) :
Nat.dist (n + k) (m + k) = Nat.dist n m
theorem Nat.dist_add_add_left (k : ) (n : ) (m : ) :
Nat.dist (k + n) (k + m) = Nat.dist n m
theorem Nat.dist_eq_intro {n : } {m : } {k : } {l : } (h : n + m = k + l) :
theorem Nat.dist_mul_right (n : ) (k : ) (m : ) :
Nat.dist (n * k) (m * k) = Nat.dist n m * k
theorem Nat.dist_mul_left (k : ) (n : ) (m : ) :
Nat.dist (k * n) (k * m) = k * Nat.dist n m
theorem Nat.dist_eq_max_sub_min {i : } {j : } :
Nat.dist i j = max i j - min i j
theorem Nat.dist_succ_succ {i : } {j : } :
Nat.dist () () = Nat.dist i j
theorem Nat.dist_pos_of_ne {i : } {j : } :
i j0 < Nat.dist i j