OAI/Geometry/CAT0Fillings/Reconstruction/Localization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Slicing.IntegralSliceTree.isMetricCurrent line 18
2. lemma OAI.CAT0Fillings.Slicing.ae_superlevelSlice_metric_of_bounded_weak_limit line 25
3. theorem OAI.CAT0Fillings.Slicing.superlevelSlice_borel_integral_of_bounded_weak_limit line 37
4. lemma OAI.CAT0Fillings.SliceReconstruction.integral_zero_unitRepresentation line 82
5. lemma OAI.CAT0Fillings.SliceReconstruction.graph_atom_mem_iff line 93
6. lemma OAI.CAT0Fillings.SliceReconstruction.superlevelSlice_graph_action line 107
7. lemma OAI.CAT0Fillings.SliceReconstruction.joint_graph_atom_mem_iff line 165
8. lemma OAI.CAT0Fillings.SliceReconstruction.fullSlice_graph_action line 179
9. lemma OAI.CAT0Fillings.SliceReconstruction.full_graph_restriction_base_action line 226