tendsto_floor_right_pure

Mathlib.Topology.Algebra.Order.Floor

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

← MathLib Explorer

English

As arguments approach a point x from the right, the ceiling function tends to ⌈x⌉.

Русский

При подходе к x справа, ceil(x) стремится к ⌈x⌉.

LaTeX

$$$$\lim_{y \to x^+} \lceil y \rceil = \lceil x \rceil.$$$$

Lean4

theorem tendsto_floor_right_pure (n : ℤ) : Tendsto (floor : α → ℤ) (𝓝[≥] n) (pure n) := by
  simpa only [floor_intCast] using tendsto_floor_right_pure_floor (n : α)

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

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

Разделы

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

Аффилиация

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