continuousOn_fract — Mathlib

English

The fractional part fract is continuous on any unit interval since it equals x − floor x, and floor is piecewise-constant there.

Русский

Частная часть fract непрерывна на любом единичном интервале, поскольку fract = x − floor x, а floor константен на таких интервалаx.

LaTeX

$$$$\text{ContinuousOn}(\operatorname{fract},\ Ico(n, n+1))\quad(\forall n\in\mathbb{Z}).$$$$

Lean4

theorem continuousOn_fract [IsTopologicalAddGroup α] (n : ℤ) : ContinuousOn (fract : α → α) (Ico n (n + 1) : Set α) :=
  continuousOn_id.sub (continuousOn_floor n)

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