instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar

Mathlib.Topology.Algebra.Star.Unitary

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

English

The inverse operation on the unitary subtype is continuous provided the ambient star is continuous.

Русский

Обратная операция на подмножествеunitary непрерывна при непрерывности звезды на окружении.

LaTeX

$$$\mathrm{ContinuousInv}(\text{Subtype unitary } R)$$$

Lean4

instance [ContinuousStar R] : ContinuousInv (unitary R) where continuous_inv := continuous_star

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

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

Разделы

Аффилиация

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