OAI/Geometry/CylinderCovering/Simplex/Chord.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimplexChord.standardSimplex line 12
  2. theorem OAI.SimplexChord.positive_mass_eq_negative_mass line 15
  3. theorem OAI.SimplexChord.negative_mass_pos line 28
  4. theorem OAI.SimplexChord.endpoints_iff line 47
  5. theorem OAI.SimplexChord.chord_bound line 70
  6. theorem OAI.SimplexChord.endpoint_unique line 80
  7. theorem OAI.SimplexChord.intersection_homothety line 94
  8. theorem OAI.SimplexChord.maximal_chord line 127
  9. theorem OAI.SimplexChord.exists_chord_iff line 144
  10. theorem OAI.SimplexChord.intersection_empty line 163
  11. theorem OAI.SimplexChord.intersection_singleton line 171
  12. theorem OAI.SimplexChord.abs_mass_eq_twice line 186
  13. theorem OAI.SimplexChord.sum_sq_le_twice_mass_sq line 199