tendsto_inv₀_cobounded'

Mathlib.Analysis.Normed.Field.Lemmas

URI: https://scilib.ai/kg/mathlib#Filter.tendsto_inv₀_cobounded'

English

The inverse map tends from cobounded α to the nhdsWithin 0 away from zero.

Русский

Обратное отображение стремится из cobounded α в nhdsWithin 0 без нуля.

LaTeX

$$$\mathrm{Tendsto}(\mathrm{inv}, \mathrm{cobounded}(\alpha), \mathcal{N}_{\neq 0})$$$

Lean4

theorem tendsto_inv₀_cobounded' : Tendsto Inv.inv (cobounded α) (𝓝[≠] 0) :=
  inv_cobounded₀.le

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

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

Разделы

Аффилиация

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