OAI/NumberTheory/PiExponent/Ampleness/AmpleSlopeTopology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NumericalAmpleness.ampleSlopes line 11
2. def OAI.PiExponent.NumericalAmpleness.ampleThreshold line 14
3. lemma OAI.PiExponent.NumericalAmpleness.ampleSlopes_bddBelow line 16
4. lemma OAI.PiExponent.NumericalAmpleness.ampleSlopes_nonempty line 21
5. lemma OAI.PiExponent.NumericalAmpleness.ampleThreshold_nonneg line 26
6. theorem OAI.PiExponent.NumericalAmpleness.ample_of_threshold_lt line 32
7. theorem OAI.PiExponent.NumericalAmpleness.threshold_lt_of_ample line 42
8. lemma OAI.PiExponent.NumericalAmpleness.slope_zero_isAmple_iff line 53
9. lemma OAI.PiExponent.NumericalAmpleness.ampleThreshold_eq_zero_of_ample line 64