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

Nat.dist n m = n - m + (m - n)

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

Nat.dist n m = n - m + (m - n)

theorem Nat.dist_comm (n : ℕ) (m : ℕ) :

Nat.dist n m = Nat.dist m n

@[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_zero_right (n : ℕ) :

Nat.dist n 0 = n

theorem Nat.dist_zero_left (n : ℕ) :

Nat.dist 0 n = n

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) :

Nat.dist n k = Nat.dist l m

theorem Nat.dist.triangle_inequality (n : ℕ) (m : ℕ) (k : ℕ) :

Nat.dist n k ≤ Nat.dist n m + Nat.dist m k

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.succ i) (Nat.succ j) = Nat.dist i j

theorem Nat.dist_pos_of_ne {i : ℕ} {j : ℕ} :

i ≠ j → 0 < Nat.dist i j