Structures · Topology
IsometryClass
IsometryClass F α β states that F is a type of isometries.
- Defined in
- Mathlib.Topology.MetricSpace.Isometry
- Shape
- 3 explicit arguments · adds isometry
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- IsometryEquiv
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- norm_map
- IsometryClass.isometry
- nnnorm_map
- enorm_map
- IsometryClass.toIsometryEquiv
- nnnorm_map'
- norm_map'
- IsometryClass.continuous
- IsometryClass.lipschitz
- IsometryClass.toHomeomorphClass
- IsometryClass.dist_eq
- IsometryClass.toIsometryEquiv_injective
- IsometryClass.ediam_image
- enorm_map'
- IsometryClass.instCoeOutIsometryEquiv
- IsometryClass.coe_coe
- IsometryClass.toContinuousMapClass
- IsometryClass.diam_image
- IsometryClass.ediam_range
- IsometryClass.diam_range
- IsometryClass.antilipschitz
- IsometryClass.edist_eq
- IsometryClass.nndist_eq
Ancestors0
No ancestors.