starContinuousMap

Mathlib.Topology.Algebra.Star

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

English

The star operation is packaged as a continuous map.

Русский

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

LaTeX

$$$\text{starContinuousMap} : C(R,R) \text{ with } \text{continuous_star}$$$

Lean4

/-- The star operation bundled as a continuous map. -/
@[simps]
def starContinuousMap : C(R, R) :=
  ⟨star, continuous_star⟩

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

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

Разделы

Аффилиация

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