pith. machine review for the scientific record. sign in
theorem proved term proof

pure_temporal_is_timelike

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 219theorem pure_temporal_is_timelike (t : ℝ) (ht : t ≠ 0) :
 220    interval (fun i : Fin 4 => if i.val = 0 then t else 0) < 0 := by

proof body

Term-mode proof.

 221  rw [timelike_iff_subluminal]
 222  show (fun i : Fin 4 => if i.val = 0 then t else 0) (1 : Fin 4) ^ 2 +
 223       (fun i : Fin 4 => if i.val = 0 then t else 0) (2 : Fin 4) ^ 2 +
 224       (fun i : Fin 4 => if i.val = 0 then t else 0) (3 : Fin 4) ^ 2 <
 225       (fun i : Fin 4 => if i.val = 0 then t else 0) (0 : Fin 4) ^ 2
 226  norm_num; exact sq_pos_of_ne_zero ht
 227
 228/-- A purely spatial displacement is spacelike. -/

depends on (9)

Lean names referenced from this declaration's body.