pith. machine review for the scientific record. sign in
def definition def or abbrev

comparative_status

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

formal statement (Lean)

 236def comparative_status : String :=

proof body

Definition body.

 237  "✓ ComparativeRecognizer defined (RG7)\n" ++
 238  "✓ notGreaterThan, comparativeEquiv: induced relations\n" ++
 239  "✓ InducesPreorder: when comparisons give a preorder\n" ++
 240  "✓ InducesPartialOrder: when comparisons give partial order\n" ++
 241  "✓ Comparative equivalence is an equivalence relation\n" ++
 242  "✓ IsOrderCompatible: compatibility with standard recognizers\n" ++
 243  "✓ order_descends_to_quotient: order structure on quotient\n" ++
 244  "✓ SeparatesPoints: families that distinguish all configurations\n" ++
 245  "✓ MetricCompatible: when comparisons respect a metric\n" ++
 246  "✓ RecognitionDistance: pseudometric from recognition\n" ++
 247  "\n" ++
 248  "COMPARATIVE RECOGNIZERS (RG7) COMPLETE"
 249
 250#eval comparative_status
 251
 252end RecogGeom
 253end IndisputableMonolith

depends on (22)

Lean names referenced from this declaration's body.