instInvolutiveStarOfContinuousStar

English

If β is an involutive star with a continuous star, then the space of continuous maps C(α, β) inherits an involutive star: applying star twice returns the original function, pointwise.

Русский

Если β имеет инволютивную операцию звезды и непрерывную звезду, то пространство непрерывных отображений C(α,β) наследует инволютивную звезду: (f^*)^* = f для всех f.

LaTeX

$$$\mathrm{InvolutiveStar}\bigl(C(\alpha, \beta)\bigr)$$

Lean4

instance [InvolutiveStar β] [ContinuousStar β] : InvolutiveStar C(α, β) where
  star_involutive _ := ext fun _ => star_star _

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