Structures · Topology
DilationClass
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
- 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
- Dilation
How is a type an instance?
Loading the hierarchy index…
Assumed by42
- Dilation.ratio
- Dilation.edist_eq
- Dilation.antilipschitz
- Dilation.lipschitz
- Dilation.ratio_ne_zero
- Dilation.comap_cobounded
- Dilation.ratio_unique
- Dilation.isUniformInducing
- Similar.comp_left
- Dilation.dist_eq
- Dilation.ratio_of_trivial
- DilationClass.edist_eq'
- Similar.comp_right
- Similar.comp_left_iff
- Dilation.ediam_image
- Dilation.diam_image
- Dilation.nndist_eq
- Dilation.ratio_pos
- Dilation.mapsTo_eball
- Similar.comp_right_iff
- Dilation.isUniformEmbedding
- Dilation.mapsTo_closedEBall
- Dilation.ratio_unique_of_nndist_ne_zero
- Dilation.ratio_unique_of_dist_ne_zero
- Dilation.tendsto_cobounded
- Dilation.mapsTo_closedBall
- Dilation.isEmbedding
- Dilation.comp_continuousOn_iff
- Dilation.mapsTo_sphere
- Dilation.mapsTo_emetric_ball
- Dilation.ratio.congr_simp
- Dilation.mapsTo_emetric_closedBall
- Dilation.isClosedEmbedding
- Dilation.comp_continuous_iff
- Dilation.ratio_of_subsingleton
- Dilation.diam_range
- Dilation.toContinuous
- Dilation.tendsto_nhds_iff
- Dilation.ediam_range
- Congruent.comp_dilation
- Dilation.injective
- Dilation.mapsTo_ball
Ancestors0
No ancestors.