tendsto_inv₀_nhdsWithin_ne_zero

Mathlib.Analysis.Normed.Field.Lemmas

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

English

Inverse tends from nhdsWithin 0 minus zero to cobounded α.

Русский

Обратное mostrado: из nhdsWithin 0 без нуля к cobounded α.

LaTeX

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

Lean4

theorem tendsto_inv₀_nhdsWithin_ne_zero : Tendsto Inv.inv (𝓝[≠] 0) (cobounded α) :=
  inv_nhdsWithin_ne_zero.le

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

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

Разделы

Аффилиация

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