module module

`IndisputableMonolith.RecogGeom.Examples`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.Core module_import
IndisputableMonolith.RecogGeom.Indistinguishable module_import
IndisputableMonolith.RecogGeom.Quotient module_import
IndisputableMonolith.RecogGeom.Recognizer module_import

declarations in this module (21)

instance finConfigSpace L35
def discreteRecognizer L39
theorem discrete_indist_iff_eq L47
theorem discrete_singleton_cells L53
inductive Sign L65
def signOf L75
def signRecognizer L79
theorem sign_indistinguishable L86
theorem neg_indist L91
theorem neg_pos_dist L95
theorem zero_pos_dist L99
def magnitudeRecognizer L105
theorem magnitude_indistinguishable L112
theorem plus_minus_indist L117
theorem diff_magnitude_dist L121
theorem sign_distinguishes_3_neg3 L136
theorem magnitude_indist_3_neg3 L139
theorem sign_indist_3_5 L142
theorem magnitude_distinguishes_3_5 L145
theorem composition_refines L150
def examples_status L176