apply_nat_le_self — Mathlib

English

For every natural n, the absolute value of n is at most n: abv(n) ≤ n.

Русский

Для каждого натурального n выполняется неравенство abv(n) ≤ n.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\operatorname{abv}(n) \\le n$$$

Lean4

/-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`. -/
theorem apply_nat_le_self [IsOrderedRing S] (n : ℕ) : abv n ≤ n :=
  by
  cases subsingleton_or_nontrivial R
  · simp [Subsingleton.eq_zero (n : R)]
  induction n with
  | zero => simp
  | succ n hn =>
    simp only [Nat.cast_succ]
    calc
      abv (n + 1) ≤ abv n + abv 1 := abv.add_le ..
      _ = abv n + 1 := (congrArg (abv n + ·) abv.map_one)
      _ ≤ n + 1 := add_le_add_right hn 1

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