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
  • n.dist m = n - m + (m - n)
Instances For
    theorem Nat.dist_comm (n : ) (m : ) :
    n.dist m = m.dist n
    @[simp]
    theorem Nat.dist_self (n : ) :
    n.dist n = 0
    theorem Nat.eq_of_dist_eq_zero {n : } {m : } (h : n.dist m = 0) :
    n = m
    theorem Nat.dist_eq_zero {n : } {m : } (h : n = m) :
    n.dist m = 0
    theorem Nat.dist_eq_sub_of_le {n : } {m : } (h : n m) :
    n.dist m = m - n
    theorem Nat.dist_eq_sub_of_le_right {n : } {m : } (h : m n) :
    n.dist m = n - m
    theorem Nat.dist_tri_left (n : ) (m : ) :
    m n.dist m + n
    theorem Nat.dist_tri_right (n : ) (m : ) :
    m n + n.dist m
    theorem Nat.dist_tri_left' (n : ) (m : ) :
    n n.dist m + m
    theorem Nat.dist_tri_right' (n : ) (m : ) :
    n m + n.dist m
    theorem Nat.dist_zero_right (n : ) :
    n.dist 0 = n
    theorem Nat.dist_zero_left (n : ) :
    Nat.dist 0 n = n
    theorem Nat.dist_add_add_right (n : ) (k : ) (m : ) :
    (n + k).dist (m + k) = n.dist m
    theorem Nat.dist_add_add_left (k : ) (n : ) (m : ) :
    (k + n).dist (k + m) = n.dist m
    theorem Nat.dist_eq_intro {n : } {m : } {k : } {l : } (h : n + m = k + l) :
    n.dist k = l.dist m
    theorem Nat.dist.triangle_inequality (n : ) (m : ) (k : ) :
    n.dist k n.dist m + m.dist k
    theorem Nat.dist_mul_right (n : ) (k : ) (m : ) :
    (n * k).dist (m * k) = n.dist m * k
    theorem Nat.dist_mul_left (k : ) (n : ) (m : ) :
    (k * n).dist (k * m) = k * n.dist m
    theorem Nat.dist_eq_max_sub_min {i : } {j : } :
    i.dist j = max i j - min i j
    theorem Nat.dist_succ_succ {i : } {j : } :
    i.succ.dist j.succ = i.dist j
    theorem Nat.dist_pos_of_ne {i : } {j : } :
    i j0 < i.dist j