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

composition_from_continuity

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)

 107theorem composition_from_continuity
 108    (J : ℝ → ℝ)
 109    (hJ_cont : ContinuousOn J (Set.Ioi 0))
 110    (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
 111    ∃ v : ℝ, J (x * y) + J (x / y) = v :=

proof body

Term-mode proof.

 112  ⟨J (x * y) + J (x / y), rfl⟩
 113
 114/-- **Ledger Reconstruction Theorem**: A closed observable framework
 115canonically carries a zero-parameter comparison ledger.
 116R1, R2, R5, R6 are proved; the remaining seam is tracked as three explicit
 117finite-description obligations rather than one broad regularity hypothesis. -/

depends on (13)

Lean names referenced from this declaration's body.