44structure SpacetimeCurve where 45 path : ℝ → (Fin 4 → ℝ) 46 tangent : ℝ → (Fin 4 → ℝ) := fun lam μ => deriv (fun l => path l μ) lam
proof body
Definition body.
47 48/-! ## §2 Parallel Transport Along a Curve -/ 49 50/-- A vector field V along a curve γ is parallel-transported if 51 DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0. 52 53 This is the defining ODE for parallel transport. -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.