mkOfCompact_star — Mathlib

English

For compact α, C(α, β) forms a NormedStarGroup when β is a Star-structured normed group with appropriate structure.

Русский

При компактном α пространство C(α, β) образует NormedStarGroup, когда β имеет звездообразную нормированную группу с необходимой структурой.

LaTeX

$$NormedStarGroup (C(α, β)) under compactness$$

Lean4

theorem _root_.BoundedContinuousFunction.mkOfCompact_star [CompactSpace α] (f : C(α, β)) :
    mkOfCompact (star f) = star (mkOfCompact f) :=
  rfl

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