`BookProof.ChapterGravitySplit.split_unique` (v x s : Fin 4 → ℝ) (c : ℝ) (hv : minkSq v = -1) (hs : minkForm s v = 0) (hx : x = s + c • v) : s = spatialPart v x ∧ c • v = timePart

Initializing...

`BookProof.ChapterGravitySplit.split_unique` (v x s : Fin 4 → ℝ) (c : ℝ) (hv : minkSq v = -1) (hs : minkForm s v = 0) (hx : x = s + c • v) : s = spatialPart v x ∧ c • v = timePart · Prove2Me