natCast_ceil_eq_intCast_ceil — Mathlib

English

If a ≥ 0, then the ceiling of a, as a natural, cast to the ring equals the ceiling of a: (⌈a⌉_+ : R) = ⌈a⌉.

Русский

Если a ≥ 0, то потолок a, приведенный к кольцу, равен потолку самого числа: (⌈a⌉_+ : R) = ⌈a⌉.

LaTeX

$$$$ 0 \le a \Rightarrow (\lceil a \rceil_+ : R) = \lceil a \rceil $$$$

Lean4

theorem natCast_ceil_eq_intCast_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : R) = ⌈a⌉ := by
  rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]

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