natCast_ceil_eq_intCast_ceil_of_neg_one_lt

English

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

Русский

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

LaTeX

$$$$ (-1 < a) \Rightarrow (\lceil a \rceil_+ : R) = \lceil a \rceil $$$$

Lean4

theorem natCast_ceil_eq_intCast_ceil_of_neg_one_lt (ha : -1 < a) : (⌈a⌉₊ : R) = ⌈a⌉ := by
  rw [← Int.natCast_ceil_eq_ceil_of_neg_one_lt ha, Int.cast_natCast]

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