continuousOn_floor — Mathlib

English

For every integer n, the floor function is constant on the half-open interval [n, n+1), hence it is continuous there.

Русский

Для каждого целого числа n функция floor на полуинтервале [n, n+1) является константной, следовательно, непрерывна там.

LaTeX

$$$$\forall n \in \mathbb{Z},\ \forall x \in [n, n+1),\ \lfloor x \rfloor = n.$$$$

Lean4

theorem continuousOn_floor (n : ℤ) : ContinuousOn (fun x => floor x : α → α) (Ico n (n + 1) : Set α) :=
  (continuousOn_congr <| floor_eq_on_Ico' n).mpr continuousOn_const

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