Theorems · Theorem · general topology

Dilation.dist_eq

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

Defined in

Mathlib.Topology.MetricSpace.Dilation

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpacePseudoMetricSpaceFunLikeDilationClass