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

P_uniqueness

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)

 215theorem P_uniqueness (P Q : ℝ → ℝ → ℝ)
 216    (hP : ∀ x y : ℝ, 0 < x → 0 < y →
 217      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y))
 218    (hQ : ∀ x y : ℝ, 0 < x → 0 < y →
 219      Cost.Jcost (x * y) + Cost.Jcost (x / y) = Q (Cost.Jcost x) (Cost.Jcost y)) :
 220    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = Q u v := by

proof body

Term-mode proof.

 221  intro u v hu hv
 222  have hP' := rcl_unconditional P hP u v hu hv
 223  have hQ' := rcl_unconditional Q hQ u v hu hv
 224  rw [hP', hQ']
 225
 226end Unconditional
 227end DAlembert
 228end Foundation
 229end IndisputableMonolith

depends on (2)

Lean names referenced from this declaration's body.