dist_eq_max_sub_min — Mathlib

English

For all i,j ∈ ℕ, dist(i,j) = max(i,j) − min(i,j).

Русский

Для любых i,j ∈ ℕ верно: dist(i,j) = max(i,j) − min(i,j).

LaTeX

$$$$ dist(i,j) = \max(i,j) - \min(i,j). $$$$

Lean4

theorem dist_eq_max_sub_min {i j : ℕ} : dist i j = (max i j) - min i j :=
  Or.elim (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 (Nat.le_of_lt h)])
    (by intro h; rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h])

Похожие утверждения