continuousOn_inv₀

Mathlib.Topology.Algebra.GroupWithZero

URI: https://scilib.ai/kg/mathlib#continuousOn_inv₀

English

The inversion map is continuous on the complement of {0}.

Русский

Обратная операция непрерывна на множестве, являющемся дополнением до нуля.

LaTeX

$$$\\mathrm{ContinuousOn}(\\mathrm{Inv.inv},\\; \\{0\\}^{c})$$$

Lean4

theorem continuousOn_inv₀ : ContinuousOn (Inv.inv : G₀ → G₀) {0}ᶜ := fun _x hx =>
  (continuousAt_inv₀ hx).continuousWithinAt

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

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

Разделы

Аффилиация

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