natCast_floor_eq_floor — Mathlib

English

If a ≥ 0, then the natural floor of a, viewed as an integer, equals the integer floor of a: (⌊a⌋_+ : ℤ) = ⌊a⌋.

Русский

Если a ≥ 0, то естественный целочисленный пол a равен целочисленному полу a: (⌊a⌋_+ : ℤ) = ⌊a⌋.

LaTeX

$$$$ 0 \le a \Rightarrow (\lfloor a \rfloor_+ : \mathbb{Z}) = \lfloor a \rfloor $$$$

Lean4

theorem natCast_floor_eq_floor (ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋ := by
  rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]

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