Theorems · Definition · general topology

BoundedContinuousFunction.mkOfCompact

{α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → [CompactSpace α] → C(α, β) → BoundedContinuousFunction α β

A continuous function on a compact space is automatically a bounded continuous function.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

21 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpaceCompactSpace