OAI/Topology/Homotopy/FiberKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nontrivial homotopy kernels from finite cardinality bounds.

  1. theorem OAI.NearbyLagrangian.HomotopyFiber.nontrivial_kernel_of_large_fiber line 20
  2. theorem OAI.NearbyLagrangian.HomotopyFiber.nontrivial_pi9_kernel_of_source_sizes line 41