Theorems · Definition · general topology

BoundedContinuousFunction.extend

{α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        {δ : Type u_2} →
          [inst_2 : TopologicalSpace δ] →
            [DiscreteTopology δ] →
              (α ↪ δ) → BoundedContinuousFunction α β → BoundedContinuousFunction δ β → BoundedContinuousFunction δ β

A version of Function.extend for bounded continuous maps. We assume that the domain has discrete topology, so we only need to verify boundedness.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpaceTopologicalSpaceDiscreteTopology