module module

`IndisputableMonolith.RecogGeom.Indistinguishable`

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 (6)

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

IndisputableMonolith.RecogGeom.Dimension module_import
IndisputableMonolith.RecogGeom.Examples module_import
IndisputableMonolith.RecogGeom.Foundations module_import
IndisputableMonolith.RecogGeom.Integration module_import
IndisputableMonolith.RecogGeom.Quotient module_import
IndisputableMonolith.RecogGeom.ZornRefinement module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.Recognizer module_import

declarations in this module (14)

def Indistinguishable L33
theorem indistinguishable_equivalence L56
def indistinguishableSetoid L62
def ResolutionCell L71
theorem mem_resolutionCell_self L75
theorem resolutionCell_eq_fiber L79
theorem resolutionCell_eq_iff L85
theorem resolutionCells_partition L103
def LocalResolution L115
theorem localResolution_covers L119
def Distinguishable L134
theorem distinguishable_iff_not_indistinguishable L138
theorem exists_distinguishable L142
def indistinguishable_status L148