pith. machine review for the scientific record. sign in
def definition def or abbrev

finite_resolution_status

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

formal statement (Lean)

 167def finite_resolution_status : String :=

proof body

Definition body.

 168  "✓ HasFiniteLocalResolution defined (RG4)\n" ++
 169  "✓ HasFiniteResolution: global finite resolution\n" ++
 170  "✓ finite_resolution_event_in_finite\n" ++
 171  "✓ finite_resolution_mono: inheritance by smaller neighborhoods\n" ++
 172  "✓ no_injection_on_infinite_finite: key non-injection theorem\n" ++
 173  "✓ finite_resolution_not_injective: corollary\n" ++
 174  "✓ eventCount, minResolution: counting distinct events\n" ++
 175  "✓ physical_interpretation_finite_resolution\n" ++
 176  "\n" ++
 177  "FINITE RESOLUTION (RG4) COMPLETE"
 178
 179#eval finite_resolution_status
 180
 181end RecogGeom
 182end IndisputableMonolith

depends on (11)

Lean names referenced from this declaration's body.