abbrev definition def or abbrev

`CognitiveState`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  43abbrev CognitiveState : Type := Sense × Emotion × MemorySystem

Definition body.

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

cognitiveStateCount in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
CognitiveStateSpaceCert in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
emotionProj_surj in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
memoryProj_surj in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
notCollapsedToEmotion in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
notCollapsedToMemory in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
notCollapsedToPair1 in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
notCollapsedToPair2 in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
notCollapsedToPair3 in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
notCollapsedToSense in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
senseProj_surj in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use

Lean names referenced from this declaration's body.

Emotion in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
MemorySystem in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use
Sense in IndisputableMonolith.CrossDomain.CognitiveStateSpace decl_use