Theorems · Definition · general topology

BoundedContinuousFunction.domRestrict

{α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → BoundedContinuousFunction α β → (s : Set α) → BoundedContinuousFunction (↑s) β

Restrict the domain of a bounded continuous function to a set.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePseudoMetricSpace