instContinuousStarSubtypeMemSubmonoidUnitary

Mathlib.Topology.Algebra.Star.Unitary

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

English

The star operation on the unitary subtype is continuous.

Русский

Операция звезды на подмножество единичных элементов непрерывна.

LaTeX

$$$\mathrm{ContinuousStar}(\text{Subtype} \; (\text{unitary } R))$$$

Lean4

instance [ContinuousStar R] : ContinuousStar (unitary R) where
  continuous_star := continuous_induced_rng.mpr continuous_subtype_val.star

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

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

Разделы

Аффилиация

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