Theorems · Definition · general topology

ContinuousMap.addEquivBoundedOfCompact

(α : Type u_1) →
  (β : Type u_2) →
    [inst : TopologicalSpace α] →
      [CompactSpace α] →
        [inst_2 : PseudoMetricSpace β] →
          [inst_3 : AddMonoid β] → [inst_4 : LipschitzAdd β] → C(α, β) ≃+ BoundedContinuousFunction α β

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

Defined in

Mathlib.Topology.ContinuousMap.Compact

Cited by

4 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCompactSpacePseudoMetricSpaceAddMonoidLipschitzAdd