OAI/Geometry/NearbyLagrangian/JetTopology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The joint jet topology and continuity of homogeneous operations.

  1. theorem OAI.NearbyLagrangian.Tubes.continuous_homogeneous_family line 17
  2. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.fderiv_zero line 70
  3. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_eval line 76
  4. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_fderiv_eval line 83
  5. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_of_joint_jet line 98
  6. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.fderiv_pullback line 106
  7. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.fderiv_directSum line 110
  8. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_pullback line 119
  9. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_directSum line 129