fact: Definition isometry {X Y : Type} (d0 : X -> X -> R) (d1 : Y -> Y -> R) (f : X -> Y) : Prop := forall x1 x2 : X, d1 (f x1) (f x2) = d0 x1 x2.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)