OAI/MathematicalPhysics/Transonic/Certificates/Window04.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SepticProfile.ExteriorCertificates.C04.power_step line 11
  2. theorem OAI.SepticProfile.ExteriorCertificates.C04.upper_eq line 86
  3. theorem OAI.SepticProfile.ExteriorCertificates.C04.rprod_eq line 161
  4. theorem OAI.SepticProfile.ExteriorCertificates.C04.rprod_pos line 235
  5. theorem OAI.SepticProfile.ExteriorCertificates.C04.mono_step line 309
  6. theorem OAI.SepticProfile.ExteriorCertificates.C04.signed_eq line 383
  7. theorem OAI.SepticProfile.ExteriorCertificates.C04.signed_zero line 458
  8. theorem OAI.SepticProfile.ExteriorCertificates.C04.signed_tail line 459
  9. theorem OAI.SepticProfile.ExteriorCertificates.C04.poly_zero line 460
  10. theorem OAI.SepticProfile.ExteriorCertificates.C04.poly_eq line 461
  11. theorem OAI.SepticProfile.ExteriorCertificates.C04.square_eq line 466
  12. theorem OAI.SepticProfile.ExteriorCertificates.C04.square_tail line 615
  13. theorem OAI.SepticProfile.ExteriorCertificates.C04.cube_eq line 616
  14. theorem OAI.SepticProfile.ExteriorCertificates.C04.cube_tail line 838
  15. theorem OAI.SepticProfile.ExteriorCertificates.C04.fourth_eq line 839
  16. theorem OAI.SepticProfile.ExteriorCertificates.C04.fourth_tail line 1134
  17. theorem OAI.SepticProfile.ExteriorCertificates.C04.powers line 1135
  18. theorem OAI.SepticProfile.ExteriorCertificates.C04.residual_eq line 1137
  19. theorem OAI.SepticProfile.ExteriorCertificates.C04.panels line 1359
  20. def OAI.SepticProfile.ExteriorCertificates.C04.window line 1393
  21. theorem OAI.SepticProfile.ExteriorCertificates.C04.window_valid line 1394
  22. theorem OAI.SepticProfile.ExteriorCertificates.C04.produces line 1426