OAI/Topology/Homotopy/CubicalNullity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cubical free nullity and change of basepoint.

  1. def OAI.NearbyLagrangian.CubicalFreeNullity.radius line 15
  2. lemma OAI.NearbyLagrangian.CubicalFreeNullity.radius_nonneg line 17
  3. lemma OAI.NearbyLagrangian.CubicalFreeNullity.radius_le_one line 19
  4. lemma OAI.NearbyLagrangian.CubicalFreeNullity.continuous_radius line 27
  5. lemma OAI.NearbyLagrangian.CubicalFreeNullity.radius_boundary line 31
  6. def OAI.NearbyLagrangian.CubicalFreeNullity.collarTime line 40
  7. lemma OAI.NearbyLagrangian.CubicalFreeNullity.continuous_collarTime line 45
  8. lemma OAI.NearbyLagrangian.CubicalFreeNullity.collarTime_zero line 49
  9. lemma OAI.NearbyLagrangian.CubicalFreeNullity.collarTime_boundary line 56
  10. lemma OAI.NearbyLagrangian.CubicalFreeNullity.denominator_pos line 63
  11. def OAI.NearbyLagrangian.CubicalFreeNullity.expand line 67
  12. lemma OAI.NearbyLagrangian.CubicalFreeNullity.continuous_expand line 70
  13. lemma OAI.NearbyLagrangian.CubicalFreeNullity.expand_zero line 79
  14. lemma OAI.NearbyLagrangian.CubicalFreeNullity.expand_mem_boundary line 84
  15. lemma OAI.NearbyLagrangian.CubicalFreeNullity.expand_boundary line 101
  16. theorem OAI.NearbyLagrangian.CubicalFreeNullity.null_of_moving_base line 110
  17. def OAI.NearbyLagrangian.CubicalFreeNullity.outerTime line 189
  18. lemma OAI.NearbyLagrangian.CubicalFreeNullity.continuous_outerTime line 195
  19. lemma OAI.NearbyLagrangian.CubicalFreeNullity.outerTime_eq_zero line 200
  20. lemma OAI.NearbyLagrangian.CubicalFreeNullity.outerTime_boundary line 208
  21. def OAI.NearbyLagrangian.CubicalFreeNullity.rebaseValue line 215
  22. lemma OAI.NearbyLagrangian.CubicalFreeNullity.continuous_rebaseValue line 219
  23. lemma OAI.NearbyLagrangian.CubicalFreeNullity.rebaseValue_zero line 230
  24. lemma OAI.NearbyLagrangian.CubicalFreeNullity.rebaseValue_boundary line 235
  25. def OAI.NearbyLagrangian.CubicalFreeNullity.rebase line 248
  26. def OAI.NearbyLagrangian.CubicalFreeNullity.rebaseHomotopy line 253