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

cosh_initials

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)

 407theorem cosh_initials : Real.cosh 0 = 1 ∧ deriv (fun x => Real.cosh x) 0 = 0 := by

proof body

Term-mode proof.

 408  constructor
 409  · simp [Real.cosh_zero]
 410  · have h := Real.deriv_cosh
 411    simp only [h, Real.sinh_zero]
 412
 413/-- **Theorem (ODE Cosh Uniqueness)**: The unique solution to H'' = H with H(0) = 1, H'(0) = 0 is cosh. -/

depends on (6)

Lean names referenced from this declaration's body.