Theorems · Definition · general topology

Isometry

{α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → (α → β) → Prop

An isometry (also known as isometric embedding) is a map preserving the edistance between pseudoemetric spaces, or equivalently the distance between pseudometric space.

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

230 results in Mathlib

Foundations

Depth 147 from the axioms, rests on 3,160 definitions · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpace