module module

`IndisputableMonolith.RecogGeom.Quotient`

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

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Papers.DraftV1 module_import
IndisputableMonolith.RecogGeom.Charts module_import
IndisputableMonolith.RecogGeom.Comparative module_import
IndisputableMonolith.RecogGeom.Composition module_import
IndisputableMonolith.RecogGeom.Connectivity module_import
IndisputableMonolith.RecogGeom.Dimension module_import
IndisputableMonolith.RecogGeom.EffectiveManifold module_import
IndisputableMonolith.RecogGeom.Examples module_import
IndisputableMonolith.RecogGeom.FiniteResolution module_import
IndisputableMonolith.RecogGeom.Foundations module_import
IndisputableMonolith.RecogGeom.Integration module_import
IndisputableMonolith.RecogGeom.RSBridge module_import
IndisputableMonolith.RecogGeom.Symmetry module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.Indistinguishable module_import

declarations in this module (14)

def RecognitionQuotient L26
def recognitionQuotientMk L30
theorem quotientMk_eq_iff L39
theorem quotientMk_respects_event L44
def quotientEventMap L56
theorem quotientEventMap_spec L60
theorem quotientEventMap_injective L64
def quotient_equiv_image L76
def liftToQuotient L89
theorem liftToQuotient_spec L94
def projectSet L101
def quotientNeighborhoods L105
theorem recognition_quotient_summary L112
def quotient_status L123