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

newton_second_law

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)

  95theorem newton_second_law (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) :
  96    standardEL m V γ t = 0 ↔ m * deriv (deriv γ) t = -(deriv V (γ t)) := by

proof body

Term-mode proof.

  97  unfold standardEL
  98  constructor
  99  · intro h; linarith
 100  · intro h; linarith
 101
 102/-- **Inertia (Newton's First Law).** When the potential is constant
 103    (`V' ≡ 0`), the EL equation reduces to `m γ̈ = 0`, i.e., constant
 104    velocity motion. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.