OAI/Geometry/CAT0Fillings/Swept/RadialChart.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CAT0Fillings.Prism.tail line 18
  2. lemma OAI.CAT0Fillings.Prism.tail_apply line 20
  3. lemma OAI.CAT0Fillings.Prism.tail_single_zero line 22
  4. lemma OAI.CAT0Fillings.Prism.tail_single_succ line 24
  5. def OAI.CAT0Fillings.Prism.zeroSumEquiv line 28
  6. lemma OAI.CAT0Fillings.Prism.zeroSumEquiv_symm_inl line 33
  7. lemma OAI.CAT0Fillings.Prism.zeroSumEquiv_symm_inr line 34
  8. def OAI.CAT0Fillings.Prism.radialForm line 37
  9. lemma OAI.CAT0Fillings.Prism.radialForm_quadratic line 42
  10. theorem OAI.CAT0Fillings.swept_radial_test_normalized_det_le line 55
  11. lemma OAI.CAT0Fillings.metric_differential_pullback line 124
  12. lemma OAI.CAT0Fillings.IntegerChart.ae_prism_tail line 153
  13. lemma OAI.CAT0Fillings.IntegerChart.paramExtended_metric_differential line 162
  14. lemma OAI.CAT0Fillings.IntegerChart.scalar_paramExtended_eqOn line 175
  15. def OAI.CAT0Fillings.IntegerChart.sweptWeight line 179
  16. lemma OAI.CAT0Fillings.IntegerChart.ae_swept_jacobian_bound line 185