instContinuousStarReal

Mathlib.Topology.Algebra.Star.Real

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

English

The real numbers carry a continuous star operation defined by the identity map.

Русский

Действительные числа оснащены непрерывной операцией звезды, заданной тождественным отображением.

LaTeX

$$$\mathrm{ContinuousStar}(\mathbb{R})$$$

Lean4

instance : ContinuousStar ℝ :=
  ⟨continuous_id⟩

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

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

Разделы

Аффилиация

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