Products of pseudometric spaces and other constructions #
This file constructs the supremum distance on binary products of pseudometric spaces and provides instances for type synonyms.
Pseudometric space structure pulled back by a function.
Equations
Instances For
Pull back a pseudometric space structure by an inducing map. This is a version of
PseudoMetricSpace.induced
useful in case if the domain already has a TopologicalSpace
structure.
Equations
Instances For
Alias of Topology.IsInducing.comapPseudoMetricSpace
.
Pull back a pseudometric space structure by an inducing map. This is a version of
PseudoMetricSpace.induced
useful in case if the domain already has a TopologicalSpace
structure.
Equations
Instances For
Pull back a pseudometric space structure by a uniform inducing map. This is a version of
PseudoMetricSpace.induced
useful in case if the domain already has a UniformSpace
structure.