natCast_ceil_eq_ceil_of_neg_one_lt

English

If a > −1, then the integer of the ceiling of a equals the ceiling of a: (⌈a⌉_+ : ℤ) = ⌈a⌉.

Русский

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

LaTeX

$$$$ (-1 < a) \Rightarrow (\lceil a \rceil_+ : \mathbb{Z}) = \lceil a \rceil $$$$

Lean4

theorem natCast_ceil_eq_ceil_of_neg_one_lt (ha : -1 < a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ := by
  rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg_of_neg_one_lt ha)]

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