instNormedStarGroup — Mathlib

English

The compactness of α yields a NormedStarGroup structure on C(α, β) with star operation continuous.

Русский

Компактность α даёт структуру NormedStarGroup на C(α, β) с непрерывной операцией звезды.

LaTeX

$$NormedStarGroup C(α,β) with star$$

Lean4

instance [CompactSpace α] : NormedStarGroup C(α, β) where
  norm_star_le
    f := by
    rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star, norm_star,
      BoundedContinuousFunction.norm_mkOfCompact]

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