Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Jeremy Avigad
! This file was ported from Lean 3 source module data.nat.dist
! leanprover-community/mathlib commit d50b12ae8e2bd910d08a94823976adae9825718b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Order.Basic
/-!
# Distance function on ℕ
This file defines a simple distance function on naturals from truncated subtraction.
-/
namespace Nat
/-- Distance (absolute value of difference) between natural numbers. -/
def dist : (n m : ℕ ) → ?m.7 n m dist ( n m : ℕ ) :=
n - m + ( m - n )
#align nat.dist Nat.dist
theorem dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n dist.def ( n m : ℕ ) : dist n m = n - m + ( m - n ) :=
rfl : ∀ {α : Sort ?u.315} {a : α }, a = a
#align nat.dist.def Nat.dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n
theorem dist_comm ( n m : ℕ ) : dist n m = dist m n := by simp [ dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , add_comm ]
#align nat.dist_comm Nat.dist_comm
@[ simp ]
theorem dist_self : ∀ (n : ℕ ), dist n n = 0 dist_self ( n : ℕ ) : dist n n = 0 := by simp [ dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , tsub_self ]
#align nat.dist_self Nat.dist_self : ∀ (n : ℕ ), dist n n = 0
theorem eq_of_dist_eq_zero : ∀ {n m : ℕ }, dist n m = 0 n = m eq_of_dist_eq_zero { n m : ℕ } ( h : dist n m = 0 ) : n = m :=
have : n - m = 0 := Nat.eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ }, n + m = 0 n = 0 h
have : n ≤ m := tsub_eq_zero_iff_le . mp : ∀ {a b : Prop }, (a ↔ b a → b this
have : m - n = 0 := Nat.eq_zero_of_add_eq_zero_left : ∀ {n m : ℕ }, n + m = 0 m = 0 h
have : m ≤ n := tsub_eq_zero_iff_le . mp : ∀ {a b : Prop }, (a ↔ b a → b this
le_antisymm ‹n ≤ m› ‹m ≤ n›
#align nat.eq_of_dist_eq_zero Nat.eq_of_dist_eq_zero : ∀ {n m : ℕ }, dist n m = 0 n = m
theorem dist_eq_zero : ∀ {n m : ℕ }, n = m dist n m = 0 dist_eq_zero { n m : ℕ } ( h : n = m ) : dist n m = 0 := by rw [ h , dist_self : ∀ (n : ℕ ), dist n n = 0 ]
#align nat.dist_eq_zero Nat.dist_eq_zero : ∀ {n m : ℕ }, n = m dist n m = 0
theorem dist_eq_sub_of_le : ∀ {n m : ℕ }, n ≤ m dist n m = m - n dist_eq_sub_of_le { n m : ℕ } ( h : n ≤ m ) : dist n m = m - n := by
rw [ dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , tsub_eq_zero_iff_le . mpr : ∀ {a b : Prop }, (a ↔ b b → a h , zero_add ]
#align nat.dist_eq_sub_of_le Nat.dist_eq_sub_of_le : ∀ {n m : ℕ }, n ≤ m dist n m = m - n
theorem dist_eq_sub_of_le_right : ∀ {n m : ℕ }, m ≤ n dist n m = n - m dist_eq_sub_of_le_right { n m : ℕ } ( h : m ≤ n ) : dist n m = n - m :=
by rw [ dist_comm ] ; apply dist_eq_sub_of_le : ∀ {n m : ℕ }, n ≤ m dist n m = m - n h
#align nat.dist_eq_sub_of_le_right Nat.dist_eq_sub_of_le_right : ∀ {n m : ℕ }, m ≤ n dist n m = n - m
theorem dist_tri_left : ∀ (n m : ℕ ), m ≤ dist n m + n dist_tri_left ( n m : ℕ ) : m ≤ dist n m + n :=
le_trans : ∀ {α : Type ?u.2645} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c le_tsub_add ( add_le_add_right ( Nat.le_add_left : ∀ (n m : ℕ ), n ≤ m + n _ _ ) _ )
#align nat.dist_tri_left Nat.dist_tri_left : ∀ (n m : ℕ ), m ≤ dist n m + n
theorem dist_tri_right : ∀ (n m : ℕ ), m ≤ n + dist n m dist_tri_right ( n m : ℕ ) : m ≤ n + dist n m := by rw [ add_comm ] ; apply dist_tri_left : ∀ (n m : ℕ ), m ≤ dist n m + n
#align nat.dist_tri_right Nat.dist_tri_right : ∀ (n m : ℕ ), m ≤ n + dist n m
theorem dist_tri_left' : ∀ (n m : ℕ ), n ≤ dist n m + m dist_tri_left' ( n m : ℕ ) : n ≤ dist n m + m := by rw [ dist_comm ] ; apply dist_tri_left : ∀ (n m : ℕ ), m ≤ dist n m + n
#align nat.dist_tri_left' Nat.dist_tri_left' : ∀ (n m : ℕ ), n ≤ dist n m + m
theorem dist_tri_right' : ∀ (n m : ℕ ), n ≤ m + dist n m dist_tri_right' ( n m : ℕ ) : n ≤ m + dist n m := by rw [ dist_comm ] ; apply dist_tri_right : ∀ (n m : ℕ ), m ≤ n + dist n m
#align nat.dist_tri_right' Nat.dist_tri_right' : ∀ (n m : ℕ ), n ≤ m + dist n m
theorem dist_zero_right : ∀ (n : ℕ ), dist n 0 = n dist_zero_right ( n : ℕ ) : dist n 0 = n :=
Eq.trans : ∀ {α : Sort ?u.3362} {a b c : α }, a = b b = c a = c ( dist_eq_sub_of_le_right : ∀ {n m : ℕ }, m ≤ n dist n m = n - m ( zero_le : ∀ (n : ℕ ), 0 ≤ n n )) ( tsub_zero n )
#align nat.dist_zero_right Nat.dist_zero_right : ∀ (n : ℕ ), dist n 0 = n
theorem dist_zero_left : ∀ (n : ℕ ), dist 0 n = n dist_zero_left ( n : ℕ ) : dist 0 n = n :=
Eq.trans : ∀ {α : Sort ?u.3470} {a b c : α }, a = b b = c a = c ( dist_eq_sub_of_le : ∀ {n m : ℕ }, n ≤ m dist n m = m - n ( zero_le : ∀ (n : ℕ ), 0 ≤ n n )) ( tsub_zero n )
#align nat.dist_zero_left Nat.dist_zero_left : ∀ (n : ℕ ), dist 0 n = n
theorem dist_add_add_right : ∀ (n k m : ℕ ), dist (n + k m + k = dist n m dist_add_add_right ( n k m : ℕ ) : dist ( n + k ) ( m + k ) = dist n m :=
calc
dist ( n + k ) ( m + k ) = n + k - ( m + k ) + ( m + k - ( n + k )) := rfl : ∀ {α : Sort ?u.3875} {a : α }, a = a
_ = n - m + ( m + k - ( n + k )) := by rw [ @ add_tsub_add_eq_tsub_right ]
_ = n - m + ( m - n ) := by rw [ @ add_tsub_add_eq_tsub_right ]
#align nat.dist_add_add_right Nat.dist_add_add_right : ∀ (n k m : ℕ ), dist (n + k m + k = dist n m
theorem dist_add_add_left : ∀ (k n m : ℕ ), dist (k + n k + m = dist n m dist_add_add_left ( k n m : ℕ ) : dist ( k + n ) ( k + m ) = dist n m := by
rw [ add_comm k n , add_comm k m ] ; apply dist_add_add_right : ∀ (n k m : ℕ ), dist (n + k m + k = dist n m
#align nat.dist_add_add_left Nat.dist_add_add_left : ∀ (k n m : ℕ ), dist (k + n k + m = dist n m
theorem dist_eq_intro : ∀ {n m k l : ℕ }, n + m = k + l dist n k = dist l m dist_eq_intro { n m k l : ℕ } ( h : n + m = k + l ) : dist n k = dist l m :=
calc
dist n k = dist ( n + m ) ( k + m ) := by n, m, k, l : ℕ h : n + m = k + l rw [ n, m, k, l : ℕ h : n + m = k + l dist_add_add_right : ∀ (n k m : ℕ ), dist (n + k m + k = dist n m n, m, k, l : ℕ h : n + m = k + l ]
_ = dist ( k + l ) ( k + m ) := by n, m, k, l : ℕ h : n + m = k + l rw [ n, m, k, l : ℕ h : n + m = k + l h n, m, k, l : ℕ h : n + m = k + l ]
_ = dist l m := by n, m, k, l : ℕ h : n + m = k + l rw [ n, m, k, l : ℕ h : n + m = k + l dist_add_add_left : ∀ (k n m : ℕ ), dist (k + n k + m = dist n m n, m, k, l : ℕ h : n + m = k + l ]
#align nat.dist_eq_intro Nat.dist_eq_intro : ∀ {n m k l : ℕ }, n + m = k + l dist n k = dist l m
theorem dist.triangle_inequality ( n m k : ℕ ) : dist n k ≤ dist n m + dist m k := by
have : dist n m + dist m k = n - m + ( m - k ) + ( k - m + ( m - n )) := by
simp [ dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , add_comm , add_left_comm , add_assoc ]
rw [ this , dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n ]
exact add_le_add : ∀ {a b c d : ℕ }, a ≤ b c ≤ d a + c ≤ b + d tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub
#align nat.dist.triangle_inequality Nat.dist.triangle_inequality : ∀ (n m k : ℕ ), dist n k ≤ dist n m + dist m k
theorem dist_mul_right : ∀ (n k m : ℕ ), dist (n * k m * k = dist n m * k dist_mul_right ( n k m : ℕ ) : dist ( n * k ) ( m * k ) = dist n m * k := by
rw [ dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , right_distrib , tsub_mul n , tsub_mul m ]
#align nat.dist_mul_right Nat.dist_mul_right : ∀ (n k m : ℕ ), dist (n * k m * k = dist n m * k
theorem dist_mul_left : ∀ (k n m : ℕ ), dist (k * n k * m = k * dist n m dist_mul_left ( k n m : ℕ ) : dist ( k * n ) ( k * m ) = k * dist n m := by
rw [ mul_comm k n , mul_comm k m , dist_mul_right : ∀ (n k m : ℕ ), dist (n * k m * k = dist n m * k , mul_comm ]
#align nat.dist_mul_left Nat.dist_mul_left : ∀ (k n m : ℕ ), dist (k * n k * m = k * dist n m
theorem dist_eq_max_sub_min { i j : ℕ } : dist i j = ( max : {α : Type ?u.10129} → [self : Max α α → α → α i j ) - min : {α : Type ?u.10144} → [self : Min α α → α → α i j :=
Or.elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c ( lt_or_ge i j )
( by intro h ; rw [ max_eq_right_of_lt h , min_eq_left_of_lt h , dist_eq_sub_of_le : ∀ {n m : ℕ }, n ≤ m dist n m = m - n ( Nat.le_of_lt : ∀ {n m : ℕ }, n < m n ≤ m h ) ] )
( by intro h ; rw [ max_eq_left h , min_eq_right h , dist_eq_sub_of_le_right : ∀ {n m : ℕ }, m ≤ n dist n m = n - m h ] )
theorem dist_succ_succ { i j : Nat } : dist ( succ i ) ( succ j ) = dist i j := by
simp [ dist.def : ∀ (n m : ℕ ), dist n m = n - m + (m - n , succ_sub_succ ]
#align nat.dist_succ_succ Nat.dist_succ_succ
theorem dist_pos_of_ne : ∀ {i j : ℕ }, i ≠ j 0 < dist i j dist_pos_of_ne { i j : Nat } : i ≠ j → 0 < dist i j := fun hne =>
Nat.lt_by_cases : ∀ {a b : ℕ } {C : Sort ?u.12091}, (a < b C (a = b C (b < a C C
( fun h : i < j => by i, j : ℕ hne : i ≠ j h : i < j rw [ i, j : ℕ hne : i ≠ j h : i < j dist_eq_sub_of_le : ∀ {n m : ℕ }, n ≤ m dist n m = m - n ( le_of_lt : ∀ {α : Type ?u.12137} [inst : Preorder α a b : α }, a < b a ≤ b h ) i, j : ℕ hne : i ≠ j h : i < j ] i, j : ℕ hne : i ≠ j h : i < j ; i, j : ℕ hne : i ≠ j h : i < j i, j : ℕ hne : i ≠ j h : i < j apply tsub_pos_of_lt h )
( fun h : i = j => by i, j : ℕ hne : i ≠ j h : i = j contradiction ) fun h : i > j => by
i, j : ℕ hne : i ≠ j h : i > j rw [ i, j : ℕ hne : i ≠ j h : i > j dist_eq_sub_of_le_right : ∀ {n m : ℕ }, m ≤ n dist n m = n - m ( le_of_lt : ∀ {α : Type ?u.12255} [inst : Preorder α a b : α }, a < b a ≤ b h ) i, j : ℕ hne : i ≠ j h : i > j ] i, j : ℕ hne : i ≠ j h : i > j ; i, j : ℕ hne : i ≠ j h : i > j i, j : ℕ hne : i ≠ j h : i > j apply tsub_pos_of_lt h
#align nat.dist_pos_of_ne Nat.dist_pos_of_ne : ∀ {i j : ℕ }, i ≠ j 0 < dist i j
end Nat