module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle
show as:
view Lean formalization →
used by (2)
depends on (1)
declarations in this module (12)
-
theorem
PRCJCostDistanceIncrementDisplay_formula -
theorem
increment_display_lt_of_sq_lt -
theorem
sq_lt_of_display_lt_delta -
theorem
PRCJCostDistanceIncrementTriangleTarget_proved -
theorem
PRCJCostDistanceVerifierTriangleTarget_proved -
theorem
PRCNullDistanceSetoidTarget_proved -
theorem
PRCJCostDistanceTriangleModulusTarget_proved -
theorem
PRCNullDistanceTransitiveTarget_proved -
def
PRCRealNullClosed -
def
ofRat -
structure
PRCJCostDistanceIncrementTriangleCertificate -
theorem
prc_jcost_distance_increment_triangle_certificate