tendsto_ceil_left — Mathlib

English

Ceiling function is continuous on left unit neighborhoods around integers: as x approaches from the left of n, ceil x tends to ⌈x⌉.

Русский

Функция ceil непрерывна слева в окрестностях целых чисел; при подходе слева к n, ceil x стремится к ⌈x⌉.

LaTeX

$$$$\forall n \in \mathbb{Z},\ Tendsto \lceil x \rceil \ (\mathcal{N}_{x}^{<}) \ (\text{unit neighborhood}) \ to \lceil x \rceil.$$$$

Lean4

theorem tendsto_ceil_left (n : ℤ) : Tendsto (fun x => ceil x : α → α) (𝓝[≤] n) (𝓝[≤] n) :=
  ((tendsto_pure_pure _ _).comp (tendsto_ceil_left_pure n)).mono_right <| pure_le_nhdsWithin le_rfl

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