OAI/Computability/PerfectCompleteness/Decoding/CutProjectionGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.CutProjectionGeometry.sourceProjection_eq_cast line 18
2. theorem OAI.PerfectCompleteness.CutProjectionGeometry.HPullback_eq_cast line 32
3. theorem OAI.PerfectCompleteness.CutProjectionGeometry.squarePullback_eq_cast line 48
4. theorem OAI.PerfectCompleteness.CutProjectionGeometry.arraysPullback_eq_cast line 65
5. theorem OAI.PerfectCompleteness.CutProjectionGeometry.rawPullback_eq_cast line 82
6. theorem OAI.PerfectCompleteness.CutProjectionGeometry.childPullback_heq line 104
7. theorem OAI.PerfectCompleteness.CutProjectionGeometry.keep_heq line 125
8. theorem OAI.PerfectCompleteness.CutProjectionGeometry.fillProjection_outside line 130