Theorems · Inductive type · general topology
IsIsometricSMul
(M : Type u) → (X : Type w) → [PseudoEMetricSpace X] → [SMul M X] → Prop
A multiplicative action is isometric if each map x ↦ c • x is an isometry.
- Cited by
- 74 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- PseudoEMetricSpaceSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PseudoEMetricSpacestatement · cited by 1,536
Cited by82
Results whose statement or proof uses this declaration.
- IsIsometricSMul.isometry_smulstatement and proof · cited by 10
- IsometryEquiv.constSMulstatement and proof · cited by 8
- IsometryEquiv.invstatement and proof · cited by 8
- edist_inv_invstatement and proof · cited by 6
- dist_mul_leftstatement and proof · cited by 5
- dist_mul_rightstatement and proof · cited by 5
- IsometryEquiv.divLeftstatement and proof · cited by 5
- IsometryEquiv.mulRightstatement and proof · cited by 4
- isometry_mul_leftstatement and proof · cited by 3
- Metric.preimage_smul_closedEBallstatement and proof · cited by 3
- Metric.preimage_smul_eballstatement and proof · cited by 3
- Metric.smul_closedBallstatement and proof · cited by 3