Theorems · Inductive type · general topology

BoundedContinuousFunction

(α : Type u) → (β : Type v) → [TopologicalSpace α] → [PseudoMetricSpace β] → Type (max u v)

α →ᵇ β is the type of bounded continuous functions α → β from a topological space to a metric space. When possible, instead of parametrizing results over (f : α →ᵇ β), you should parametrize over (F : Type*) [BoundedContinuousMapClass F α β] (f : F). When you extend this structure, make sure to extend BoundedContinuousMapClass.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

511 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpacePseudoMetricSpace