tendsto_floor_left_pure_sub_one — Mathlib

English

The fractional part fract is continuous on unit intervals; near integers from the left, fract tends to ceil(x) − 1.

Русский

Частная часть fract непрерывна на единичных интервалах; слева от целых fract стремится к ceil(x) − 1.

LaTeX

$$$$\lim_{y \to x^-} \operatorname{fract}(y) = 1 - 0 = 0 \quad\text{(modularly understood within unit interval)}.$$$$

Lean4

theorem tendsto_floor_left_pure_sub_one (n : ℤ) : Tendsto (floor : α → ℤ) (𝓝[<] n) (pure (n - 1)) := by
  simpa only [ceil_intCast] using tendsto_floor_left_pure_ceil_sub_one (n : α)

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