OAI/Geometry/Manifold/ProjectiveSphere.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EinsteinFour.FourSpace line 14

    Also declared: ComparatorChallenges/EinsteinFour.lean:12 (same declaration text).

  2. abbrev OAI.EinsteinFour.I4 line 15

    Also declared: ComparatorChallenges/EinsteinFour.lean:13 (same declaration text).

  3. def OAI.EinsteinFour.coordinateVector line 18

    Also declared: ComparatorChallenges/EinsteinFour.lean:15 (same declaration text).

  4. abbrev OAI.EinsteinFour.RoundSphere4 line 21

    Also declared: ComparatorChallenges/EinsteinFour.lean:17 (same declaration text).

  5. abbrev OAI.EinsteinFour.ComplexProjective2 line 24

    Also declared: ComparatorChallenges/EinsteinFour.lean:19 (same declaration text).

  6. abbrev OAI.EinsteinFour.RealProjective4 line 27

    Also declared: ComparatorChallenges/EinsteinFour.lean:21 (same declaration text).

  7. def OAI.EinsteinFour.roundDistance line 30

    Also declared: ComparatorChallenges/EinsteinFour.lean:23 (same declaration text).

  8. def OAI.EinsteinFour.fubiniStudyDistance line 35

    Also declared: ComparatorChallenges/EinsteinFour.lean:26 (same declaration text).

  9. def OAI.EinsteinFour.realProjectiveDistance line 40

    Also declared: ComparatorChallenges/EinsteinFour.lean:29 (same declaration text).

  10. abbrev OAI.EinsteinFour.SmoothMetric line 49

    Also declared: ComparatorChallenges/EinsteinFour.lean:37 (same declaration text).

  11. def OAI.EinsteinFour.metricInChart line 56

    Also declared: ComparatorChallenges/EinsteinFour.lean:42 (same declaration text).

  12. def OAI.EinsteinFour.partialDeriv line 63

    Also declared: ComparatorChallenges/EinsteinFour.lean:48 (same declaration text).

  13. def OAI.EinsteinFour.christoffel line 68

    Also declared: ComparatorChallenges/EinsteinFour.lean:51 (same declaration text).

  14. def OAI.EinsteinFour.curvatureComponent line 77

    Also declared: ComparatorChallenges/EinsteinFour.lean:58 (same declaration text).

  15. def OAI.EinsteinFour.ricciInChart line 86

    Also declared: ComparatorChallenges/EinsteinFour.lean:66 (same declaration text).

  16. def OAI.EinsteinFour.sectionalNumerator line 92

    Also declared: ComparatorChallenges/EinsteinFour.lean:70 (same declaration text).

  17. def OAI.EinsteinFour.IsEinstein line 99

    Also declared: ComparatorChallenges/EinsteinFour.lean:76 (same declaration text).

  18. def OAI.EinsteinFour.HasPositiveSectionalCurvature line 105

    Also declared: ComparatorChallenges/EinsteinFour.lean:81 (same declaration text).

  19. def OAI.EinsteinFour.scaledEDistance line 111

    Also declared: ComparatorChallenges/EinsteinFour.lean:85 (same declaration text).

  20. def OAI.EinsteinFour.ScaledIsometricTo line 117

    Also declared: ComparatorChallenges/EinsteinFour.lean:89 (same declaration text).

  21. abbrev OAI.EinsteinFour.UnitSphere line 131
  22. def OAI.EinsteinFour.antipode line 134
  23. theorem OAI.EinsteinFour.antipode_val line 137
  24. theorem OAI.EinsteinFour.antipode_antipode line 139
  25. theorem OAI.EinsteinFour.unitSphere_ne_zero line 143
  26. theorem OAI.EinsteinFour.antipode_ne_self line 150
  27. theorem OAI.EinsteinFour.sphere_involution_antipodal line 164
  28. theorem OAI.EinsteinFour.round_distance_preserving_inner line 205
  29. theorem OAI.EinsteinFour.free_round_involution_eq_antipode line 222
  30. theorem OAI.EinsteinFour.normalized_inner_smul line 237
  31. theorem OAI.EinsteinFour.normalized_inner_mk_rep line 250
  32. theorem OAI.EinsteinFour.fubiniStudyDistance_mk line 261
  33. theorem OAI.EinsteinFour.realProjectiveDistance_mk line 267
  34. def OAI.EinsteinFour.sphereToProjective line 278
  35. theorem OAI.EinsteinFour.sphereToProjective_surjective line 282
  36. theorem OAI.EinsteinFour.sphereToProjective_eq_iff line 295
  37. def OAI.EinsteinFour.antipodalSetoid line 321
  38. def OAI.EinsteinFour.antipodalQuotientEquiv line 334
  39. theorem OAI.EinsteinFour.antipodalQuotientEquiv_mk line 347
  40. theorem OAI.EinsteinFour.realProjectiveDistance_sphere line 353
  41. theorem OAI.EinsteinFour.realProjectiveDistance_eq_min line 361
  42. theorem OAI.EinsteinFour.free_round_involution_projective_fibers_and_distance line 374