tendsto_fract_left — Mathlib

English

The fract function tends to 1 as x approaches from left to integers, and to 0 as x tends to infinity.

Русский

fract стремится к 1 слева от целых чисел, и к 0 при возрастании x.

LaTeX

$$$$\text{Tendsto}(\operatorname{fract}, x^-\to 1, x^+\to 0)$$$$

Lean4

theorem tendsto_fract_left [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) :
    Tendsto (fract : α → α) (𝓝[<] n) (𝓝[<] 1) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ (tendsto_fract_left' _) (Eventually.of_forall fract_lt_one)

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