OAI/Geometry/SplitTangent/FamilyPropagationStep.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Family Propagation Step.

  1. structure OAI.SplitTangent.TangentSplitting.LocalFamilyTransport line 20
  2. theorem OAI.SplitTangent.TangentSplitting.exists_local_family_transport line 40
  3. abbrev OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.frame line 73
  4. def OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map line 77
  5. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_self line 81
  6. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_fixed line 89
  7. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_holomorphic_at line 120
  8. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_projector line 171
  9. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_cocycle line 179
  10. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_reverse_comp line 200
  11. theorem OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_eq_of_horizontal_germ line 214
  12. theorem OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_eq_on_ball_of_horizontal_germ line 288
  13. lemma OAI.SplitTangent.TangentSplitting.coordinate_covariantDerivative_change line 338
  14. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_horizontal line 417
  15. lemma OAI.SplitTangent.TangentSplitting.LocalChartImages.continuationMap_coordinates_analytic line 446
  16. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_eq_continuationMap line 468
  17. lemma OAI.SplitTangent.TangentSplitting.family_slice_holomorphic line 511
  18. abbrev OAI.SplitTangent.TangentSplitting.shiftedFamily line 516
  19. lemma OAI.SplitTangent.TangentSplitting.shiftedFamily_holomorphic line 519
  20. abbrev OAI.SplitTangent.TangentSplitting.familyContinuation line 531
  21. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.map_eq_familyContinuation_shift line 535
  22. lemma OAI.SplitTangent.TangentSplitting.LocalFamilyTransport.familyContinuation_holomorphic_at_local line 587
  23. lemma OAI.SplitTangent.TangentSplitting.familyContinuation_cocycle line 629
  24. lemma OAI.SplitTangent.TangentSplitting.familyContinuation_holomorphic_at_const_end line 636
  25. theorem OAI.SplitTangent.TangentSplitting.familyContinuation_holomorphic_at line 685