Theorems · Inductive type · general topology

DilationClass

(F : Type u_3) →
  (α : outParam (Type u_4)) →
    (β : outParam (Type u_5)) → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → [FunLike F α β] → Prop

DilationClass F α β r states that F is a type of r-dilations. You should extend this typeclass when you extend Dilation.

Defined in

Mathlib.Topology.MetricSpace.Dilation

Cited by

41 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

PseudoEMetricSpacePseudoEMetricSpaceFunLike