Mathlib Map

Structures · Topology

DilationEquivClass

Typeclass saying that F is a type of bundled equivalences such that all e : F are dilations.

Defined in
Mathlib.Topology.MetricSpace.DilationEquiv
Shape
3 explicit arguments · adds edist_eq'

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances1

  • DilationEquiv

How is a type an instance?

Loading the hierarchy index…

Assumed by3

Ancestors0

No ancestors.