natCast_ceil_eq_ceil — Mathlib

English

If a ≥ 0, then the integer of the natural-ceiling of a equals the ordinary ceiling: (⌈a⌉_+ : ℤ) = ⌈a⌉.

Русский

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

LaTeX

$$$$ 0 \le a \Rightarrow (\lceil a \rceil_+ : \mathbb{Z}) = \lceil a \rceil $$$$

Lean4

theorem natCast_ceil_eq_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ := by
  rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]

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