continuousAt_inv

Mathlib.Topology.Algebra.Group.Basic

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

English

Inv.inv is continuous at every a ∈ G.

Русский

Функция Inv.inv непрерывна в любой точке a ∈ G.

LaTeX

$$$\\\\operatorname{ContinuousAt} \\\\operatorname{Inv.inv} a.$$$

Lean4

@[to_additive]
theorem continuousAt_inv {x : G} : ContinuousAt Inv.inv x :=
  continuous_inv.continuousAt

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

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

Разделы

Аффилиация

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