Theorems · Theorem · general topology

DilationEquiv.mk.inj

∀ {X : Type u_1} {Y : Type u_2} {inst : PseudoEMetricSpace X} {inst_1 : PseudoEMetricSpace Y} {toEquiv : X ≃ Y}
  {edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = ↑r * edist x y} {toEquiv_1 : X ≃ Y}
  {edist_eq'_1 : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv_1.toFun x) (toEquiv_1.toFun y) = ↑r * edist x y},
  { toEquiv := toEquiv, edist_eq' := edist_eq' } = { toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 } →
    toEquiv = toEquiv_1

Defined in

Mathlib.Topology.MetricSpace.DilationEquiv

Cited by

1 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound