addEquivBoundedOfCompact — Mathlib

English

When α is compact and β is an additive monoid with Lipschitz addition, there is an additive bijection between C(α,β) and the bounded continuous maps α →ᵇ β.

Русский

Пусть α компактен и β — аддитивный полугрупп с липшицевым сложением; существует аддитивное биективное соответствие между C(α,β) и α →ᵇ β.

LaTeX

$$$\;C(\alpha, \beta) \cong_+ (\alpha \to^b \beta)$$$

Lean4

/-- When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
additively equivalent to `C(α, 𝕜)`.
-/
@[simps! -fullyApplied apply symm_apply]
def addEquivBoundedOfCompact [AddMonoid β] [LipschitzAdd β] : C(α, β) ≃+ (α →ᵇ β) :=
  ({ toContinuousMapAddHom α β, (equivBoundedOfCompact α β).symm with } : (α →ᵇ β) ≃+ C(α, β)).symm

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