OAI/Geometry/NearbyLagrangian/CoreEndpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Restored central endpoints after compact Hamiltonian transport.

  1. theorem OAI.NearbyLagrangian.Transport.exists_core_restored_endpoint line 24