inv_tendsto_nhdsGT_zero

Mathlib.Topology.Algebra.Order.Field

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

English

If f tends to 0 from above in nhdsWithin 0 (Ioi 0), then f^{-1} tends to 0 as well (in nhds 0).

Русский

Если f стремится к 0 сверху в nhdsWithin 0 (Ioi 0), то 1/f также стремится к 0.

LaTeX

$$$\text{Tendsto}(f)\; (nhdsWithin 0 (Ioi 0)) \Rightarrow \text{Tendsto}(f^{-1})\; (nhds 0).$$$

Lean4

theorem inv_tendsto_nhdsGT_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop :=
  tendsto_inv_nhdsGT_zero.comp h

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

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

Разделы

Аффилиация

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