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

affine_reparametrization

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)

  76theorem affine_reparametrization (g : MetricTensor) (geo : NullGeodesic g) (a b : ℝ)
  77    (ha : a ≠ 0) :
  78    let lam' := fun lam => a * lam + b

proof body

Tactic-mode proof.

  79    ∃ geo' : NullGeodesic g, ∀ lam, geo'.path lam = geo.path (lam' lam) := by
  80  classical
  81  intro lam'
  82  refine ⟨{
  83    path := fun lam => geo.path (lam' lam)
  84    null_condition := ?null
  85    geodesic_equation := ?geoEq
  86  }, ?_⟩
  87  · intro lam
  88    simpa [lam'] using geo.null_condition (lam' lam)
  89  · intro lam μ
  90    simpa [lam'] using geo.geodesic_equation (lam' lam) μ
  91  · intro lam; rfl
  92

depends on (5)

Lean names referenced from this declaration's body.