continuousOn_inv

Mathlib.Topology.Algebra.Group.Basic

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

English

For every subset s of G, the inverse map Inv.inv is continuous on s.

Русский

Для любого множества s в G отображение Inv.inv непрерывно на s.

LaTeX

$$$\\\\operatorname{ContinuousOn} \\\\operatorname{Inv.inv} s.$$$

Lean4

@[to_additive]
theorem continuousOn_inv {s : Set G} : ContinuousOn Inv.inv s :=
  continuous_inv.continuousOn

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

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

Разделы

Аффилиация

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