module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy`

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 (5)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCategoryTheoryParse module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCFullZFCParse module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCSetTheoryParse module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCShrunkCertificate module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCTypeTheoryParse module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCInevitabilityInstances module_import

declarations in this module (12)

def Degenerate L54
def Discriminating L57
def ExprReflexive L61
def RealizesDelta L65
theorem not_degenerate_iff_discriminating L68
theorem realizesDelta_of_discriminating L80
theorem not_degenerate_of_realizesDelta L97
theorem distinction_dichotomy L105
theorem distinction_not_optional L117
theorem prcFormalSystem_exprReflexive L129
theorem ofTwoDistinct_exprReflexive L132
theorem named_foundations_not_degenerate L138