Theorems · Definition · general topology

Dilation.ratio

{α : Type u_1} →
  {β : Type u_2} →
    {F : Type u_4} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : FunLike F α β] → [DilationClass F α β] → F → NNReal

The ratio of a dilation f. If the ratio is undefined (i.e., the distance between any two points in α is either zero or infinity), then we choose one as the ratio.

Defined in

Mathlib.Topology.MetricSpace.Dilation

Cited by

43 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpaceFunLikeDilationClass