OAI/Topology/Homotopy/HomotopyFiber.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

The path-space homotopy fiber and exactness at its projection.

  1. def OAI.NearbyLagrangian.HomotopyFiber.Fiber line 18
  2. instance OAI.NearbyLagrangian.HomotopyFiber.(instance at line 21) line 21
  3. def OAI.NearbyLagrangian.HomotopyFiber.base line 24
  4. def OAI.NearbyLagrangian.HomotopyFiber.projection line 27
  5. theorem OAI.NearbyLagrangian.HomotopyFiber.projection_base line 30
  6. def OAI.NearbyLagrangian.HomotopyFiber.projectionNullhomotopy line 35
  7. def OAI.NearbyLagrangian.HomotopyFiber.liftNullhomotopy line 48
  8. theorem OAI.NearbyLagrangian.HomotopyFiber.projection_liftNullhomotopy line 62
  9. theorem OAI.NearbyLagrangian.HomotopyFiber.kernel_eq_projection_range line 66
  10. def OAI.NearbyLagrangian.HomotopyFiber.frontTime line 98
  11. def OAI.NearbyLagrangian.HomotopyFiber.backTime line 99
  12. lemma OAI.NearbyLagrangian.HomotopyFiber.continuous_frontTime line 101
  13. lemma OAI.NearbyLagrangian.HomotopyFiber.continuous_backTime line 105
  14. lemma OAI.NearbyLagrangian.HomotopyFiber.frontTime_zero_right line 115
  15. lemma OAI.NearbyLagrangian.HomotopyFiber.backTime_one_right line 120
  16. lemma OAI.NearbyLagrangian.HomotopyFiber.backTime_zero_left line 125
  17. lemma OAI.NearbyLagrangian.HomotopyFiber.frontTime_seam line 131
  18. lemma OAI.NearbyLagrangian.HomotopyFiber.backTime_seam line 136
  19. def OAI.NearbyLagrangian.HomotopyFiber.deformValue line 145
  20. lemma OAI.NearbyLagrangian.HomotopyFiber.continuous_deformValue line 149
  21. lemma OAI.NearbyLagrangian.HomotopyFiber.deformValue_start line 167
  22. lemma OAI.NearbyLagrangian.HomotopyFiber.deformValue_end line 172
  23. lemma OAI.NearbyLagrangian.HomotopyFiber.deformValue_zero line 179
  24. def OAI.NearbyLagrangian.HomotopyFiber.deformPath line 188
  25. def OAI.NearbyLagrangian.HomotopyFiber.deformFiber line 191
  26. lemma OAI.NearbyLagrangian.HomotopyFiber.deformFiber_zero line 195
  27. def OAI.NearbyLagrangian.HomotopyFiber.loopInclusion line 202
  28. lemma OAI.NearbyLagrangian.HomotopyFiber.loopInclusion_base line 206
  29. def OAI.NearbyLagrangian.HomotopyFiber.loopRepresentative line 208
  30. def OAI.NearbyLagrangian.HomotopyFiber.deformHomotopy line 219
  31. lemma OAI.NearbyLagrangian.HomotopyFiber.deformValue_fixed line 228
  32. lemma OAI.NearbyLagrangian.HomotopyFiber.deformFiber_fixed line 236
  33. lemma OAI.NearbyLagrangian.HomotopyFiber.loopRepresentative_fixed line 243
  34. def OAI.NearbyLagrangian.HomotopyFiber.boundaryRepresentative line 264
  35. def OAI.NearbyLagrangian.HomotopyFiber.boundaryRepresentativeHomotopy line 275
  36. theorem OAI.NearbyLagrangian.HomotopyFiber.projection_loopInclusion line 289
  37. theorem OAI.NearbyLagrangian.HomotopyFiber.projection_kernel_eq_loop_range line 294