IndisputableMonolith.RecogGeom.ZornRefinement

declarations in this module (20)

• def recognizerSetoid L39
• theorem recognizerSetoid_iff L43
• theorem composite_setoid_iff L55
• theorem composite_setoid_le_left L62
• theorem composite_setoid_le_right L68
• theorem composite_setoid_is_inf L80
• def IsFinerThan L101
• theorem isFinerThan_refl L105
• theorem isFinerThan_trans L109
• theorem composite_isFinerThan_left L116
• theorem composite_isFinerThan_right L121
• theorem composite_isFinerThan_glb L127
• def IsRecognizerInduced L144
• def ChainInfClosed L153
• theorem maximal_recognizer_setoid_exists L165
• def IsMaximalRecognizer L186
• theorem maximal_cells_unsplittable L193
• theorem maximal_unique_setoid L205
• theorem recognizer_meet_semilattice L224
• def zorn_refinement_status L242