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

null_geodesic_exists_minkowski

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)

  68theorem null_geodesic_exists_minkowski (ic : InitialConditions) :
  69    ∃ geo : NullGeodesic minkowski_tensor,
  70      geo.path 0 = ic.position ∧
  71      (∀ μ, deriv (fun lam => geo.path lam μ) 0 = ic.direction μ) := by

proof body

Term-mode proof.

  72  refine ⟨straight_null_geodesic ic, ?_, ?_⟩
  73  · simp [straight_null_geodesic, straight_line]
  74  · intro μ; simp [straight_null_geodesic, straight_line]
  75

depends on (5)

Lean names referenced from this declaration's body.