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

indistinguishable_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)

 148def indistinguishable_status : String :=

proof body

Definition body.

 149  "✓ Indistinguishable relation defined (RG3)\n" ++
 150  "✓ Proved: reflexivity, symmetry, transitivity\n" ++
 151  "✓ Proved: indistinguishable_equivalence\n" ++
 152  "✓ ResolutionCell defined (equivalence classes)\n" ++
 153  "✓ Proved: resolutionCell_eq_fiber\n" ++
 154  "✓ Proved: resolutionCells_partition\n" ++
 155  "✓ LocalResolution defined\n" ++
 156  "✓ Distinguishable defined\n" ++
 157  "\n" ++
 158  "INDISTINGUISHABILITY (RG3) COMPLETE"
 159
 160#eval indistinguishable_status
 161
 162end RecogGeom
 163end IndisputableMonolith

depends on (9)

Lean names referenced from this declaration's body.