continuousAt_fract — Mathlib

English

If x is not an integer, fract is continuous at x.

Русский

Если x не целое, fract непрерывна в x.

LaTeX

$$$$\text{ContinuousAt}(\operatorname{fract}, x)\quad\text{whenever } x \notin \mathbb{Z}.$$$

Lean4

theorem continuousAt_fract [OrderClosedTopology α] [IsTopologicalAddGroup α] {x : α} (h : x ≠ ⌊x⌋) :
    ContinuousAt fract x :=
  (continuousOn_fract ⌊x⌋).continuousAt <| Ico_mem_nhds ((floor_le _).lt_of_ne h.symm) (lt_floor_add_one _)

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