floor_int — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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