module module

`IndisputableMonolith.RecogGeom.Charts`

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

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

IndisputableMonolith.RecogGeom.Integration module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.FiniteResolution module_import
IndisputableMonolith.RecogGeom.Quotient module_import

declarations in this module (17)

structure RecognitionChart L57
theorem chart_respects_equiv L76
def chartOnQuotient L82
theorem chartOnQuotient_well_defined L91
def ChartCompatible L104
theorem chartCompatible_refl L109
theorem chartCompatible_symm L116
structure RecognitionAtlas L125
theorem atlas_covers_quotient L134
def hasRecognitionDimension L147
def recognition_dimension_unique_hypothesis L155
theorem recognition_dimension_unique L159
def finite_resolution_no_chart_hypothesis L178
theorem finite_resolution_no_chart L184
theorem chart_exists_implies L193
def IsSmoothRecognitionGeometry L212
def charts_status L239