module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCInevitabilityInstances`

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

used by (1)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FormalSystem module_import

declarations in this module (14)

theorem length_le_of_extends L52
def ofTwoDistinct L65
theorem ofTwoDistinct_expressive L75
theorem two_distinct_realizes_delta L83
def boolLogicSystem L88
theorem boolLogicSystem_expressive L90
theorem boolLogicSystem_embeds_delta L96
def peanoSystem L110
theorem peanoSystem_embeds_delta L112
def setFoundationSystem L118
theorem setFoundationSystem_embeds_delta L121
def typeTheorySystem L127
theorem typeTheorySystem_embeds_delta L130
theorem named_foundations_embed_delta L139