not_tendsto_nhds_of_tendsto_atBot

Mathlib.Topology.Order.OrderClosed

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

English

If Tendsto f l atBot, then Tendsto f l to nhds a is impossible for any a.

Русский

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

LaTeX

$$Tendsto f l atBot ∧ Tendsto f l (nhds a) → False$$

Lean4

theorem not_tendsto_nhds_of_tendsto_atBot (hf : Tendsto f l atBot) (a : α) : ¬Tendsto f l (𝓝 a) :=
  hf.not_tendsto (disjoint_nhds_atBot a).symm

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

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

Разделы

Аффилиация

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