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

configDimUniversalityCert

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)

 115def configDimUniversalityCert : ConfigDimUniversalityCert where
 116  sensory_5 := sensory_hasConfigDim5

proof body

Definition body.

 117  emotion_5 := emotion_hasConfigDim5
 118  biological_5 := biological_hasConfigDim5
 119  economic_5 := economic_hasConfigDim5
 120  linguistic_5 := linguistic_hasConfigDim5
 121  triple_125 := fun _ _ _ _ _ _ => triple_product_125
 122  five_domain_3125 := five_domain_product
 123  five_pow_five := fivePowFive
 124
 125end IndisputableMonolith.CrossDomain.ConfigDimUniversality

depends on (9)

Lean names referenced from this declaration's body.