IndisputableMonolith.RecogGeom.Composition

declarations in this module (19)

• def CompositeRecognizer L40
• theorem composite_R_eq L57
• theorem composite_indistinguishable_iff L61
• theorem composite_refines_left L68
• theorem composite_refines_right L74
• theorem composite_distinguishes L80
• theorem composite_resolutionCell L94
• theorem composite_cell_subset_left L101
• theorem composite_cell_subset_right L106
• def quotientMapLeft L114
• def quotientMapRight L120
• theorem quotientMapLeft_surjective L126
• theorem quotientMapRight_surjective L133
• theorem refinement_theorem L154
• theorem composite_comm_events L162
• theorem composite_comm_indistinguishable L167
• theorem composite_info_monotone_left L192
• theorem composite_info_monotone_right L197
• def composition_status L204