Smooth Riemannian isometries #
A smooth Riemannian isometry is a diffeomorphism whose differential preserves the inner product on each tangent space. The inverse and composite are again smooth Riemannian isometries. This is the natural map for transporting the Levi-Civita connection and geodesics.
The pointwise condition says that the pullback of the metric on the target is the metric on the
source; see J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Chapter 2. Isometries
preserve tangent-vector norms and the Riemannian length pathELength of every curve.
structure
TauCeti.RiemannianIsometry
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
(I : ModelWithCorners ℝ E H)
(J : ModelWithCorners ℝ F H')
(M : Type u_7)
(N : Type u_8)
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
extends Diffeomorph I J M N ↑⊤ :
Type (max u_7 u_8)
An infinitely differentiable equivalence that preserves the Riemannian inner product of tangent vectors. Smoothness of the inverse is part of the underlying diffeomorphism.
- toFun : M → N
- invFun : N → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- contMDiff_toFun : ContMDiff I J ↑⊤ ⇑self.toEquiv
- contMDiff_invFun : ContMDiff J I ↑⊤ ⇑self.symm
- inner_mfderiv' (x : M) (v w : TangentSpace I x) : inner ℝ ((mfderiv% ⇑self.toDiffeomorph x) v) ((mfderiv% ⇑self.toDiffeomorph x) w) = inner ℝ v w
Instances For
@[instance_reducible]
noncomputable instance
TauCeti.RiemannianIsometry.instEquivLike
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
:
EquivLike (RiemannianIsometry I J M N) M N
theorem
TauCeti.RiemannianIsometry.ext
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{Φ Ψ : RiemannianIsometry I J M N}
(h : ∀ (x : M), Φ x = Ψ x)
:
theorem
TauCeti.RiemannianIsometry.ext_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{Φ Ψ : RiemannianIsometry I J M N}
:
@[simp]
theorem
TauCeti.RiemannianIsometry.coe_toDiffeomorph
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.inner_mfderiv
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
(x : M)
(v w : TangentSpace I x)
:
The differential of a Riemannian isometry preserves inner products.
@[simp]
theorem
TauCeti.RiemannianIsometry.norm_mfderiv
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
(x : M)
(v : TangentSpace I x)
:
The differential of a Riemannian isometry preserves tangent-vector norms.
@[simp]
theorem
TauCeti.RiemannianIsometry.enorm_mfderiv
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
(x : M)
(v : TangentSpace I x)
:
The differential of a Riemannian isometry preserves extended tangent-vector norms.
theorem
TauCeti.RiemannianIsometry.mdifferentiable
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
MDiff ⇑Φ
A smooth Riemannian isometry is differentiable everywhere.
theorem
TauCeti.RiemannianIsometry.mdifferentiableAt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
(x : M)
:
MDiffAt ⇑Φ x
A smooth Riemannian isometry is differentiable at each point.
noncomputable def
TauCeti.RiemannianIsometry.refl
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
:
RiemannianIsometry I I M M
The identity diffeomorphism is a Riemannian isometry.
Instances For
@[simp]
theorem
TauCeti.RiemannianIsometry.refl_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
(x : M)
:
noncomputable def
TauCeti.RiemannianIsometry.symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
RiemannianIsometry J I N M
The inverse of a smooth Riemannian isometry.
Instances For
@[simp]
theorem
TauCeti.RiemannianIsometry.symm_toDiffeomorph
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
The underlying diffeomorphism of the inverse Riemannian isometry is the inverse of the underlying diffeomorphism.
theorem
TauCeti.RiemannianIsometry.coe_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
The inverse Riemannian isometry has the same underlying function as the inverse of its underlying diffeomorphism.
@[simp]
theorem
TauCeti.RiemannianIsometry.symm_apply_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
(x : M)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.apply_symm_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
(y : N)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.symm_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.symm_refl
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
:
The inverse of the identity isometry is the identity isometry.
noncomputable def
TauCeti.RiemannianIsometry.trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{H'' : Type u_8}
[TopologicalSpace H'']
{K : ModelWithCorners ℝ G H''}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace H'' P]
[Bundle.RiemannianBundle fun (z : P) => TangentSpace K z]
(Φ : RiemannianIsometry I J M N)
(Ψ : RiemannianIsometry J K N P)
:
RiemannianIsometry I K M P
The composite of two smooth Riemannian isometries.
Instances For
@[simp]
theorem
TauCeti.RiemannianIsometry.trans_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{H'' : Type u_8}
[TopologicalSpace H'']
{K : ModelWithCorners ℝ G H''}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace H'' P]
[Bundle.RiemannianBundle fun (z : P) => TangentSpace K z]
(Φ : RiemannianIsometry I J M N)
(Ψ : RiemannianIsometry J K N P)
(x : M)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.symm_trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{H'' : Type u_8}
[TopologicalSpace H'']
{K : ModelWithCorners ℝ G H''}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace H'' P]
[Bundle.RiemannianBundle fun (z : P) => TangentSpace K z]
(Φ : RiemannianIsometry I J M N)
(Ψ : RiemannianIsometry J K N P)
:
The inverse of a composite is the composite of the inverses in reverse order.
@[simp]
theorem
TauCeti.RiemannianIsometry.refl_trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.trans_refl
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.self_trans_symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.symm_trans_self
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
theorem
TauCeti.RiemannianIsometry.trans_assoc
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{H'' : Type u_8}
[TopologicalSpace H'']
{K : ModelWithCorners ℝ G H''}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace H'' P]
[Bundle.RiemannianBundle fun (z : P) => TangentSpace K z]
(Φ : RiemannianIsometry I J M N)
(Ψ : RiemannianIsometry J K N P)
{L : Type u_10}
[NormedAddCommGroup L]
[NormedSpace ℝ L]
{H''' : Type u_11}
[TopologicalSpace H''']
{K' : ModelWithCorners ℝ L H'''}
{Q : Type u_12}
[TopologicalSpace Q]
[ChartedSpace H''' Q]
[Bundle.RiemannianBundle fun (z : Q) => TangentSpace K' z]
(Θ : RiemannianIsometry K K' P Q)
:
@[simp]
theorem
TauCeti.RiemannianIsometry.pathELength_comp
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
{γ : ℝ → M}
{a b : ℝ}
:
A smooth Riemannian isometry preserves the Riemannian length of any curve.