tendsto_fract_left' — Mathlib

English

As x grows, fract converges toward 0 from above with respect to the fractional part.

Русский

При росте x fract сходится к 0 сверху.

LaTeX

$$$$\lim_{x \to +\infty} \operatorname{fract}(x) = 0.$$$$

Lean4

theorem tendsto_fract_left' [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) :
    Tendsto (fract : α → α) (𝓝[<] n) (𝓝 1) :=
  by
  rw [← sub_sub_cancel (n : α) 1]
  refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_
  exact tendsto_floor_left' n

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