OAI/Geometry/Relativity/CKS/TailSymbols.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSADM.eventually_norm_ge line 12
  2. lemma OAI.CKSADM.eventually_norm_gt line 15
  3. lemma OAI.CKSADM.spatial_eventually_nhds line 18
  4. lemma OAI.CKSADM.spatial_pd_congr line 26
  5. lemma OAI.CKSADM.TailRegular.pd line 31
  6. lemma OAI.CKSADM.TailRegular.mul line 35
  7. lemma OAI.CKSADM.TailRegular.add line 40
  8. lemma OAI.CKSADM.TailRegular.congr line 45
  9. lemma OAI.CKSADM.Decay.congr line 50
  10. lemma OAI.CKSADM.Decay.zero line 57
  11. lemma OAI.CKSADM.Decay.const line 60
  12. lemma OAI.CKSADM.Decay.add line 63
  13. lemma OAI.CKSADM.Decay.mul line 71
  14. lemma OAI.CKSADM.Decay.weaken line 85
  15. lemma OAI.CKSADM.SymbolN.congr line 91
  16. lemma OAI.CKSADM.SymbolN.zero line 97
  17. lemma OAI.CKSADM.SymbolN.const line 105
  18. lemma OAI.CKSADM.SymbolN.weaken line 113
  19. lemma OAI.CKSADM.SymbolN.add line 119
  20. lemma OAI.CKSADM.SymbolN.lower line 130
  21. lemma OAI.CKSADM.SymbolN.mul line 136
  22. lemma OAI.CKSADM.Symbol.const line 155
  23. lemma OAI.CKSADM.Symbol.congr line 158
  24. lemma OAI.CKSADM.Symbol.add line 162
  25. lemma OAI.CKSADM.Symbol.mul line 166
  26. lemma OAI.CKSADM.Symbol.weaken line 170
  27. lemma OAI.CKSADM.Symbol.pd line 173
  28. lemma OAI.CKSADM.Symbol.const_mul line 176
  29. lemma OAI.CKSADM.Symbol.neg line 180
  30. lemma OAI.CKSADM.Symbol.sub line 183
  31. lemma OAI.CKSADM.pd_inverse line 187
  32. lemma OAI.CKSADM.SymbolN.inverse line 196
  33. lemma OAI.CKSADM.Symbol.inverse line 225