Theorems · Inductive type · general topology

DilationEquiv

(X : Type u_1) → (Y : Type u_2) → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → Type (max u_1 u_2)

Type of equivalences X ≃ Y such that ∀ x y, edist (f x) (f y) = r * edist x y for some r : ℝ≥0, r ≠ 0.

Defined in

Mathlib.Topology.MetricSpace.DilationEquiv

Cited by

55 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

PseudoEMetricSpacePseudoEMetricSpace