tendsto_ceil_left_pure

Mathlib.Topology.Algebra.Order.Floor

URI: https://scilib.ai/kg/mathlib#tendsto_ceil_left_pure

← MathLib Explorer

English

As x approaches from the left to n, floor x tends to ⌊x⌋ cast minus one, i.e., ⌈x⌉ − 1.

Русский

При подходе слева к n, floor x стремится к ⌈x⌉ − 1.

LaTeX

$$$$\lim_{y \to x^-} \lfloor y \rfloor = \lceil x \rceil - 1.$$$$

Lean4

theorem tendsto_ceil_left_pure (n : ℤ) : Tendsto (ceil : α → ℤ) (𝓝[≤] n) (pure n) := by
  simpa only [ceil_intCast] using tendsto_ceil_left_pure_ceil (n : α)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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