tendsto_ceil_right_pure_add_one — Mathlib

English

The floor function approaches ⌊x⌋ from below with the addition of one, i.e., floor x near x from above matches ⌊x⌋ + 0.

Русский

Пол приближается к ⌊x⌋ слева с добавлением единицы; около x сверху floor x соответствует ⌊x⌋.

LaTeX

$$$$\lim_{y \to x^+} \big\lfloor y \big\rfloor = \big\lfloor x \big\rfloor.$$$$

Lean4

theorem tendsto_ceil_right_pure_add_one (n : ℤ) : Tendsto (ceil : α → ℤ) (𝓝[>] n) (pure (n + 1)) := by
  simpa only [floor_intCast] using tendsto_ceil_right_pure_floor_add_one (n : α)

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