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

ControllerState

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)

 171structure ControllerState where
 172  area : ℝ
 173  demand : ℝ
 174  entropy : ℝ
 175  entropyFloor : ℝ
 176  attention : ℝ
 177  signature : ℝ
 178  signatureMin : ℝ
 179  signatureMax : ℝ
 180  z : ℝ
 181  hArea : 0 < area
 182  hDemand : 0 < demand
 183
 184/-- The full critical-loading condition. -/

used by (4)

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

depends on (3)

Lean names referenced from this declaration's body.