lean_workbook_plus_13994
OpenProve that is increasing
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13994 (f : ℝ → ℝ) (h : f = fun t ↦ 4^t + 9^t) : ∀ t₁ t₂, t₁ < t₂ → f t₁ < f t₂ := by sorry
Source
Prove that is increasing
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_13994 (f : ℝ → ℝ) (h : f = fun t ↦ 4^t + 9^t) : ∀ t₁ t₂, t₁ < t₂ → f t₁ < f t₂ := by sorry