OAI/Geometry/CAT0Fillings/Prism/TimeCoordinate.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CAT0Fillings.IntegerChart.ae_prism_fderiv_timeline 35 - lemma
OAI.CAT0Fillings.IntegerChart.ae_prism_jacobian_timeline 50 - lemma
OAI.CAT0Fillings.IntegerChart.lipschitz_timeline 77 - lemma
OAI.CAT0Fillings.IntegerChart.lipschitz_sliceline 82 - lemma
OAI.CAT0Fillings.IntegerChart.boundedLip_sliceline 87