pith. machine review for the scientific record. sign in
structure definition def or abbrev

CostAlgPlusObj

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)

 321structure CostAlgPlusObj where
 322  κ : ℝ
 323  κ_pos : 0 < κ
 324
 325/-- The cost attached to an object of `CostAlg⁺`. -/
 326noncomputable def CostAlgPlusObj.cost (C : CostAlgPlusObj) : ℝ → ℝ :=

proof body

Definition body.

 327  costFamily C.κ
 328
 329/-- Morphisms in `CostAlg⁺` are the positive exponents `α > 0` satisfying
 330    the parameter relation `α κ₂ = κ₁`. This is the paper's
 331    order-preserving morphism classification. -/

used by (15)

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

depends on (14)

Lean names referenced from this declaration's body.