theorem proved term proof

`primitive_to_uniqueness_aczel`

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

formal statement (Lean)

 116theorem primitive_to_uniqueness_aczel [AczelSmoothnessPackage] (F : ℝ → ℝ)
 117    (hF : PrimitiveCostHypotheses F) :
 118    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=

proof body

Term-mode proof.

 119  primitive_to_uniqueness_of_kernel F hF (aczelRegularityKernel (H F))
 120
 121end FunctionalEquation
 122end Cost
 123end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
AczelSmoothnessPackage in IndisputableMonolith.Cost.AczelClass decl_use
aczelRegularityKernel in IndisputableMonolith.Cost.AczelClassification decl_use
PrimitiveCostHypotheses in IndisputableMonolith.Cost.AczelClassification decl_use
primitive_to_uniqueness_of_kernel in IndisputableMonolith.Cost.AczelClassification decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use