OAI/Geometry/CAT0Fillings/Slicing/EuclideanSplit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CAT0Fillings.Prism.Euc line 28
2. def OAI.CAT0Fillings.Prism.splitLinear line 30
3. def OAI.CAT0Fillings.Prism.split line 38
4. lemma OAI.CAT0Fillings.Prism.split_apply line 41
5. lemma OAI.CAT0Fillings.Prism.split_symm_apply line 44
6. lemma OAI.CAT0Fillings.Prism.split_measurePreserving line 47
7. lemma OAI.CAT0Fillings.Prism.split_symm_measurePreserving line 59
8. lemma OAI.CAT0Fillings.Prism.integral_split line 63
9. lemma OAI.CAT0Fillings.Prism.split_single_zero line 67
10. lemma OAI.CAT0Fillings.Prism.split_single_succ line 70