Theorems · Theorem · general topology

Dilation.nndist_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 : α),
  nndist (f x) (f y) = Dilation.ratio f * nndist x y

Defined in

Mathlib.Topology.MetricSpace.Dilation

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpacePseudoMetricSpaceFunLikeDilationClass