Theorems · Theorem · general topology
AddMonoidHomClass.isometry_of_norm
∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
[inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕), (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑fAlias of the reverse direction of AddMonoidHomClass.isometry_iff_norm.
- Defined in
- Mathlib.Analysis.Normed.Group.Uniform
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Realstatement · cited by 25,697
- Norm.normstatement · cited by 5,413
- FunLikestatement and proof · cited by 2,560
- SeminormedAddGroupstatement and proof · cited by 331
- AddMonoidHomClassstatement and proof · cited by 252
- Isometrystatement · cited by 230
- AddMonoidHomClass.isometry_iff_normproof · cited by 5
Cited by18
Results whose statement or proof uses this declaration.
- LinearIsometry.isometryproof · cited by 24
- SemilinearIsometryClass.isometryproof · cited by 8
- Unitization.isometry_inrproof · cited by 7
- star_isometryproof · cited by 6
- RingHom.isometryproof · cited by 4
- gelfandTransform_isometryproof · cited by 2
- NumberField.InfinitePlace.isometry_embeddingproof · cited by 2
- NumberField.InfinitePlace.isometry_embedding_of_isRealproof · cited by 2
- WithLp.unitization_isometry_inrproof · cited by 1
- MeasureTheory.Lp.isometry_compMeasurePreservingproof · cited by 1
- MeasureTheory.hausdorffMeasure_smul_right_imageproof · cited by 1
- NumberField.InfinitePlace.LiesOver.isometry_algebraMapproof · cited by 1