lean_workbook_plus_11236
ProvedProfit function will be
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11236 (x : ℝ) (R C : ℝ → ℝ) (P : ℝ → ℝ) (h₁ : P = R - C) : P x = R x - C x := by sorry
Source
Profit function will be
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11236 (x : ℝ) (R C : ℝ → ℝ) (P : ℝ → ℝ) (h₁ : P = R - C) : P x = R x - C x := by sorry