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 nhds of 0.

Русский

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

LaTeX

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

Lean4

theorem tendsto_inv₀_cobounded : Tendsto Inv.inv (cobounded α) (𝓝 0) :=
  tendsto_inv₀_cobounded'.mono_right inf_le_left

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

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

Разделы

Аффилиация

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