theorem proved term proof

`costCompose_sub_left`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 490theorem costCompose_sub_left (a b₁ b₂ : ℝ) :
 491    a ★ b₁ - a ★ b₂ = (2 * a + 2) * (b₁ - b₂) := by

Term-mode proof.

 492  unfold costCompose
 493  ring
 494
 495/-- Equation (2.6): left-cancellation holds on the nonnegative cost range. -/

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

costCompose_left_cancel in IndisputableMonolith.Algebra.CostAlgebra decl_use

Lean names referenced from this declaration's body.