eventually_const_lt

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.eventually_const_lt

← MathLib Explorer

English

If Tendsto f l (nhds a) then Tendsto f l atBot cannot hold.

Русский

Если Tendsto f l (nhds a), тогда Tendsto f l к atBot невозможно.

LaTeX

$$Tendsto f l (nhds a) ⇒ ¬Tendsto f l atBot$$

Lean4

theorem eventually_const_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (𝓝 v)) :
    ∀ᶠ a in l, u < f a :=
  h.eventually <| eventually_gt_nhds hv

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

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

Разделы

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

Аффилиация

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