OAI/Geometry/CAT0Fillings/Reconstruction/GraphAssembly.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Slicing.boundedLip_of_lipschitz_compact line 21
2. def OAI.CAT0Fillings.Slicing.outerCutoff line 27
3. lemma OAI.CAT0Fillings.Slicing.outerCutoff_lipschitz line 31
4. lemma OAI.CAT0Fillings.Slicing.outerCutoff_eq_one line 45
5. lemma OAI.CAT0Fillings.Slicing.outerCutoff_support line 51
6. lemma OAI.CAT0Fillings.Slicing.restrict_zero_separated line 59
7. lemma OAI.CAT0Fillings.Slicing.boundary_restrict_zero_separated line 75
8. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_zero_separated line 100
9. lemma OAI.CAT0Fillings.Slicing.unitRepresentation_atoms_on_level line 140
10. lemma OAI.CAT0Fillings.SliceReconstruction.atomCode_atoms_injective line 229
11. lemma OAI.CAT0Fillings.SliceReconstruction.selectedAtom_on_level line 242
12. theorem OAI.CAT0Fillings.SliceReconstruction.exists_compact_bilipschitz_scalar_atom_graphs line 251