Theorems · Theorem · general topology

Dilation.ratio_unique_of_dist_ne_zero

∀ {α : Type u_6} {β : Type u_7} {F : Type u_5} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
  dist x y ≠ 0 → dist (f x) (f y) = ↑r * dist x y → r = Dilation.ratio f

The ratio is equal to the distance ratio for any two points with nonzero finite distance; dist version

Defined in

Mathlib.Topology.MetricSpace.Dilation

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpacePseudoMetricSpaceFunLikeDilationClass