module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField`

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

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Kernel module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealMulBoundedContinuity module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle module_import

declarations in this module (31)

abbrev PRCRawRatLedger L23
def PRCRawCauchy L27
def PRCRawNullEquivalent L33
def raw L41
theorem raw_cauchy L44
theorem raw_apply L47
def PRCRawAdd L53
def PRCRawNeg L57
def PRCRawMul L61
def PRCRawEventuallyLe L65
theorem PRCJCostDistance_add_right L72
theorem PRCJCostDistance_add_left L79
theorem PRCJCostDistance_neg_neg L86
def PRCRealAddClosureTarget L94
def PRCRealAddCongruenceTarget L98
def PRCRealNegClosureTarget L108
def PRCRealNegCongruenceTarget L112
def PRCRealMulClosureTarget L119
def PRCRealMulCongruenceTarget L124
def PRCRealOrderCongruenceTarget L134
def PRCRawEventuallyClose L142
def PRCRealRepresentativeCauchy L149
def PRCRealRepresentativeLimit L156
def PRCRealCompletenessTarget L165
theorem PRCRealAddClosureTarget_proved L171
theorem PRCRealNegClosureTarget_proved L195
theorem PRCRealAddCongruenceTarget_proved L205
theorem PRCRealNegCongruenceTarget_proved L228
structure PRCRealCompleteOrderedFieldTargets L310
structure PRCRealCompleteOrderedFieldConditionalCertificate L323
theorem prc_real_complete_ordered_field_conditional_certificate L343