OAI/NumberTheory/PiExponent/Ampleness/NumericalAmpleness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.NumericalAmpleness.open_eq_top_of_subsingleton line 13
2. theorem OAI.PiExponent.NumericalAmpleness.exists_global_frame_of_top_frame line 19
3. theorem OAI.PiExponent.NumericalAmpleness.isAmple_of_subsingleton line 34
4. theorem OAI.PiExponent.NumericalAmpleness.isAmple_of_integral_dimension_zero line 51
5. structure OAI.PiExponent.NumericalAmpleness.IntegralCurve line 60
6. theorem OAI.PiExponent.NumericalAmpleness.no_integralCurve_of_dimension_zero line 69