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)
74structure StrictConvexityFromClosure (J : ℝ → ℝ) : Prop where
75 strict_convex : StrictConvexOn ℝ (Set.Ioi 0) J
76
77/-- Calibration obligation extracted from the unit-choice seam. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
extracted
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
Calibration
in IndisputableMonolith.Foundation.CostAxioms
decl_use
-
Calibration
in IndisputableMonolith.Foundation.CostFromDistinction
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use