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

H_continuous_of_positive_continuous

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)

  65private theorem H_continuous_of_positive_continuous (F : ℝ → ℝ)
  66    (hCont : ContinuousOn F (Set.Ioi 0)) : Continuous (H F) := by

proof body

Term-mode proof.

  67  have h := ContinuousOn.comp_continuous hCont Real.continuous_exp
  68  have h' : Continuous (fun t => F (Real.exp t)) :=
  69    h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
  70  have h_add : Continuous (fun t : ℝ => F (Real.exp t) + (1 : ℝ)) :=
  71    h'.add (continuous_const : Continuous fun _ : ℝ => (1 : ℝ))
  72  simpa [H, G] using h_add
  73

used by (1)

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.