OAI/Geometry/NearbyLagrangian/TubeKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The tube-family reduction from a classifying map and homotopy-size hypotheses.

  1. theorem OAI.NearbyLagrangian.Tubes.telescope_negative_class_iff_classifying_zero line 19
  2. theorem OAI.NearbyLagrangian.Tubes.kernelFamilyGoal_of_classifying_map_and_source_sizes line 51