Structures · Topology
IsIsometricVAdd
An additive action is isometric if each map x ↦ c +ᵥ x is an isometry.
- Shape
- 2 explicit arguments · adds isometry_vadd
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- DomAddAct
- AddUnits
- Prod
- ULift
- AddOpposite
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by101
- IsIsometricVAdd.isometry_vadd
- IsometryEquiv.constVAdd
- IsometryEquiv.neg
- dist_add_right
- dist_add_left
- Metric.vadd_closedBall
- edist_neg_neg
- Metric.vadd_ball
- IsometryEquiv.addRight
- Metric.vadd_sphere
- dist_vadd
- IsometryEquiv.subLeft
- IsometryEquiv.addLeft
- isometry_add_left
- IsometryEquiv.subRight
- Metric.preimage_vadd_eball
- Metric.preimage_vadd_closedEBall
- dist_neg_neg
- edist_add_left
- Metric.preimage_vadd_closedBall
- Metric.vadd_eball
- edist_add_right
- Metric.preimage_add_right_eball
- isometry_neg
- isometry_add_right
- Metric.vadd_closedEBall
- Metric.preimage_vadd_ball
- nndist_vadd
- Metric.preimage_add_right_ball
- nndist_add_left
- IsometryEquiv.constVAdd_symm
- dist_sub_right
- Metric.preimage_add_left_closedEBall
- nndist_neg_neg
- nndist_add_right
- IsometryEquiv.subLeft_symm_apply
- Metric.infEDist_vadd
- Bornology.IsBounded.vadd
- Metric.preimage_add_left_eball
- Metric.preimage_add_right_closedEBall
- IsometryEquiv.subLeft_apply
- edist_sub_left
- Pi.isIsometricVAdd''
- edist_sub_right
- instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd
- ediam_vadd
- EMetric.preimage_add_right_ball
- IsometryEquiv.constVAdd_toEquiv
- MeasureTheory.instVAddInvariantMeasureHausdorffMeasureOfIsIsometricVAdd
- edist_vadd_left
Ancestors0
No ancestors.