instStarAddMonoid — Mathlib

English

The space of bounded continuous functions α → β carries a NormedStarGroup structure, defined coordinatewise: star (f) x = star (f x) and the star operation preserves the norm: ||f*|| = ||f||.

Русский

Пространство ограниченно непрерывных функций имеет структуру нормированной звездной группы: звезда действует по координатам и нормa сохраняется: ||f*|| = ||f||.

LaTeX

$$$$\text{NormedStarGroup}(\alpha \to^b \beta)$$ with $\|f^*\| = \|f\|$ and $(f^*)(x) = (f(x))^*.$$$

Lean4

instance instStarAddMonoid : StarAddMonoid (α →ᵇ β)
    where
  star f := f.comp star starNormedAddGroupHom.lipschitz
  star_involutive f := ext fun x => star_star (f x)
  star_add f g := ext fun x => star_add (f x) (g x)

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