equivBoundedOfCompact — Mathlib

English

When α is compact, bounded continuous maps α →ᵇ β are equivalent to continuous maps C(α, β).

Русский

Когда α компактно, ограниченные непрерывные отображения α →ᵇ β эквивалентны непрерывным отображениям C(α,β).

LaTeX

$$$C(\\alpha, \\beta) \\simeq (\\alpha \\to\\ᵇ \\beta)$ при $CompactSpace(\\alpha)$$$

Lean4

/-- When `α` is compact, the bounded continuous maps `α →ᵇ β` are
equivalent to `C(α, β)`.
-/
@[simps -fullyApplied]
def equivBoundedOfCompact : C(α, β) ≃ (α →ᵇ β) :=
  ⟨mkOfCompact, BoundedContinuousFunction.toContinuousMap, fun f =>
    by
    ext
    rfl, fun f => by
    ext
    rfl⟩

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