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

Constants

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)

  31structure Constants where
  32  Knet  : ℝ
  33  Cproj : ℝ
  34  Ceng  : ℝ
  35  Cdisp : ℝ
  36  Knet_nonneg  : 0 ≤ Knet
  37  Cproj_nonneg : 0 ≤ Cproj
  38  Ceng_nonneg  : 0 ≤ Ceng
  39  Cdisp_nonneg : 0 ≤ Cdisp
  40
  41/-- Coercivity constant `c_min = 1 / (K_net · C_proj · C_eng)`.
  42
  43We keep it as a definition (not a field) to avoid duplication. -/

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.