instStar — Mathlib

English

If β has a star operation, then ZeroAtInftyContinuousMap α β inherits a star-ring/StarAddMonoid structure in a pointwise fashion.

Русский

Если у β есть звездная операция, то ZeroAtInftyContinuousMap α β наследует звездную кольцевую/StarAddMonoid структуру по точкам.

LaTeX

$$Star(ZeroAtInftyContinuousMap α β)$$

Lean4

instance instStar : Star C₀(α, β) where
  star
    f :=
    { toFun := fun x => star (f x)
      continuous_toFun := (map_continuous f).star
      zero_at_infty' := by simpa only [star_zero] using (continuous_star.tendsto (0 : β)).comp (zero_at_infty f) }

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