tendsto_ceil_right'

Mathlib.Topology.Algebra.Order.Floor

URI: https://scilib.ai/kg/mathlib#tendsto_ceil_right'

English

The fract function tends to 0 as x approaches integers from above, in the fract-topology sense.

Русский

fract стремится к 0 при подходе слева к целым числам сверху.

LaTeX

$$$$\lim_{y \to x^+} \operatorname{fract}(y) = 0.$$$$

Lean4

theorem tendsto_ceil_right' (n : ℤ) : Tendsto (fun x => ceil x : α → α) (𝓝[>] n) (𝓝 (n + 1)) :=
  (tendsto_ceil_right n).mono_right inf_le_left

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru