tendsto_floor_right_pure_floor — Mathlib

English

As arguments approach a point x from the right, the floor function tends to the integer ⌊x⌋.

Русский

Предел floor при подходе к x справа равен целому числу ⌊x⌋.

LaTeX

$$$$\lim_{y \to x^+} \lfloor y \rfloor = \lfloor x \rfloor.$$$$

Lean4

theorem tendsto_floor_right_pure_floor (x : α) : Tendsto (floor : α → ℤ) (𝓝[≥] x) (pure ⌊x⌋) :=
  tendsto_pure.2 <|
    mem_of_superset (Ico_mem_nhdsGE <| lt_floor_add_one x) fun _y hy =>
      floor_eq_on_Ico _ _ ⟨(floor_le x).trans hy.1, hy.2⟩

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