ceil_int — Mathlib

English

For every integer z, the ceiling map to naturals coincides with converting z to a natural number.

Русский

Для каждого целого числа z функция ceil, отправляющая в натуральные числа, совпадает с преобразованием z в натуральное число.

LaTeX

$$$\\\\forall z \\\\in \\\\mathbb{Z}, \\\\operatorname{ceil}(z) \\\\equiv \\\\operatorname{toNat}(z).$$$

Lean4

@[simp]
theorem ceil_int : (Nat.ceil : ℤ → ℕ) = Int.toNat :=
  rfl

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