`zorn_refinement_status`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.ZornRefinement
domain: RecogGeom
line: 242 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.ZornRefinement on GitHub at line 242.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 239
 240/-! ## Module Status -/
 241
 242def zorn_refinement_status : String :=
 243  "✓ recognizerSetoid: Recognizer → Setoid C\n" ++
 244  "✓ composite_setoid_le_left/right: composition refines both\n" ++
 245  "✓ composite_setoid_is_inf: composition is greatest lower bound\n" ++
 246  "✓ IsFinerThan: heterogeneous refinement preorder\n" ++
 247  "✓ isFinerThan_refl, isFinerThan_trans: preorder properties\n" ++
 248  "✓ composite_isFinerThan_left/right/glb: composition as meet\n" ++
 249  "✓ maximal_recognizer_setoid_exists: ZORN'S LEMMA for recognizers\n" ++
 250  "✓ maximal_cells_unsplittable: maximal cells are stable\n" ++
 251  "✓ maximal_unique_setoid: maximal recognizers fix the partition\n" ++
 252  "✓ recognizer_meet_semilattice: connection to complete lattice\n" ++
 253  "\n" ++
 254  "ZORN'S LEMMA + RG3 REFINEMENT: COMPLETE"
 255
 256#eval zorn_refinement_status
 257
 258end ZornRefinement
 259end RecogGeom
 260end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.