OAI/Geometry/Relativity/CKS/AngularSlice.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularSlice.AP line 10
  2. abbrev OAI.CKSAngularSlice.MP line 11
  3. abbrev OAI.CKSAngularSlice.A line 12
  4. def OAI.CKSAngularSlice.injection line 14
  5. def OAI.CKSAngularSlice.slice line 16
  6. lemma OAI.CKSAngularSlice.injection_zero line 18
  7. lemma OAI.CKSAngularSlice.injection_succ line 19
  8. lemma OAI.CKSAngularSlice.slice_zero line 20
  9. lemma OAI.CKSAngularSlice.slice_succ line 21
  10. lemma OAI.CKSAngularSlice.injection_basis line 23
  11. lemma OAI.CKSAngularSlice.slice_hasFDerivAt line 29
  12. lemma OAI.CKSAngularSlice.slice_smooth line 31
  13. lemma OAI.CKSAngularSlice.D_slice line 34
  14. def OAI.CKSAngularSlice.restrictJet line 42
  15. def OAI.CKSAngularSlice.restrictThree line 44
  16. lemma OAI.CKSAngularSlice.actualScalarJet_slice line 47
  17. lemma OAI.CKSAngularSlice.actualThreeJet_slice line 65
  18. lemma OAI.CKSAngularSlice.restrictJet_norm line 80
  19. lemma OAI.CKSAngularSlice.restrictThree_norm line 93
  20. lemma OAI.CKSAngularSlice.angular_twojet_le_mixed line 100
  21. lemma OAI.CKSAngularSlice.angular_threejet_le_mixed line 105