continuousOn_ceil — Mathlib

English

For every integer n, the ceiling function is constant on the interval (n-1, n], hence it is continuous there.

Русский

Для каждого целого числа n функция ceil на интервале (n-1, n] константна, значит, непрерывна там.

LaTeX

$$$$\forall n \in \mathbb{Z},\ \forall x \in (n-1, n],\ \lceil x \rceil = n.$$$$

Lean4

theorem continuousOn_ceil [IsStrictOrderedRing α] (n : ℤ) :
    ContinuousOn (fun x => ceil x : α → α) (Ioc (n - 1) n : Set α) :=
  (continuousOn_congr <| ceil_eq_on_Ioc' n).mpr continuousOn_const

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