OAI/Analysis/SphereIsometry/AlignedConfiguration.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Aligned sphere chords

The record retains the four actual endpoint equations. Its inverse exchanges the endpoints and negates the two direction vectors literally; it uses no oddness property of the sphere isometry.

  1. structure OAI.Tingley.AlignedConfiguration line 23
  2. theorem OAI.Tingley.unit_radius_bounds_of_norm_sub line 46
  3. theorem OAI.Tingley.unit_radius_bounds_of_eq_add line 59
  4. theorem OAI.Tingley.unit_radius_bounds_of_eq_sub line 72
  5. def OAI.Tingley.AlignedConfiguration.d line 90
  6. def OAI.Tingley.AlignedConfiguration.A line 92
  7. def OAI.Tingley.AlignedConfiguration.B line 94
  8. theorem OAI.Tingley.AlignedConfiguration.d_pos line 96
  9. theorem OAI.Tingley.AlignedConfiguration.d_ne_zero line 98
  10. theorem OAI.Tingley.AlignedConfiguration.d_le_two line 100
  11. theorem OAI.Tingley.AlignedConfiguration.d_eq_s_add_u line 102
  12. theorem OAI.Tingley.AlignedConfiguration.A_pos line 104
  13. theorem OAI.Tingley.AlignedConfiguration.B_pos line 106
  14. theorem OAI.Tingley.AlignedConfiguration.A_lt_one line 108
  15. theorem OAI.Tingley.AlignedConfiguration.B_lt_one line 113
  16. theorem OAI.Tingley.AlignedConfiguration.A_add_B line 118
  17. theorem OAI.Tingley.AlignedConfiguration.A_add_B_lt_one line 126
  18. theorem OAI.Tingley.AlignedConfiguration.one_sub_B line 131
  19. theorem OAI.Tingley.AlignedConfiguration.one_sub_A line 137
  20. theorem OAI.Tingley.AlignedConfiguration.p_eq_d_mul_A line 144
  21. theorem OAI.Tingley.AlignedConfiguration.u_eq_d_mul_B line 147
  22. theorem OAI.Tingley.AlignedConfiguration.chord_identity line 150
  23. theorem OAI.Tingley.AlignedConfiguration.norm_x_sub_z line 156
  24. theorem OAI.Tingley.AlignedConfiguration.p_bounds line 165
  25. theorem OAI.Tingley.AlignedConfiguration.r_bounds line 168
  26. theorem OAI.Tingley.AlignedConfiguration.s_bounds line 171
  27. theorem OAI.Tingley.AlignedConfiguration.u_bounds line 174
  28. def OAI.Tingley.AlignedConfiguration.inverse line 178

    Source documentation

    Exchange the endpoints and literally negate both chord directions.

    def inverse : AlignedConfiguration f.symm (f y) t M where
…

    Mentions: OAI.Tingley.AlignedConfiguration

  29. theorem OAI.Tingley.AlignedConfiguration.inverse_x line 202
  30. theorem OAI.Tingley.AlignedConfiguration.inverse_z line 204
  31. theorem OAI.Tingley.AlignedConfiguration.inverse_v_coe line 206
  32. theorem OAI.Tingley.AlignedConfiguration.inverse_w_coe line 208
  33. theorem OAI.Tingley.AlignedConfiguration.inverse_p line 210
  34. theorem OAI.Tingley.AlignedConfiguration.inverse_r line 212
  35. theorem OAI.Tingley.AlignedConfiguration.inverse_s line 214
  36. theorem OAI.Tingley.AlignedConfiguration.inverse_u line 216
  37. theorem OAI.Tingley.AlignedConfiguration.inverse_d line 218
  38. theorem OAI.Tingley.AlignedConfiguration.inverse_A line 222
  39. theorem OAI.Tingley.AlignedConfiguration.inverse_B line 225