instContinuousInv

Mathlib.Topology.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#OrderDual.instContinuousInv

English

In the order dual G^{op}, the inverse map is continuous, i.e., ContinuousInv G^{op} holds.

Русский

В порядке дуала G^{op} обратное отображение непрерывно, то есть ContinuousInv G^{op}.

LaTeX

$$$\\\\operatorname{ContinuousInv} (G^{\\mathrm{op}}).$$$

Lean4

@[to_additive]
instance instContinuousInv : ContinuousInv Gᵒᵈ :=
  ‹ContinuousInv G›

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

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

Разделы

Аффилиация

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