tendsto_ceil_left_pure_ceil — Mathlib

English

As arguments approach a point x from the left, the ceiling function tends to ⌈x⌉ with respect to the corresponding left neighborhood.

Русский

При подходе к x слева, ceil(x) сходится к ⌈x⌉ в левом окрестном подходе.

LaTeX

$$$$\lim_{y \to x^-} \lceil y \rceil = \lceil x \rceil.$$$$

Lean4

theorem tendsto_ceil_left_pure_ceil (x : α) : Tendsto (ceil : α → ℤ) (𝓝[≤] x) (pure ⌈x⌉) :=
  tendsto_pure.2 <|
    mem_of_superset (Ioc_mem_nhdsLE <| sub_lt_iff_lt_add.2 <| ceil_lt_add_one _) fun _y hy =>
      ceil_eq_on_Ioc _ _ ⟨hy.1, hy.2.trans (le_ceil _)⟩

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