OAI/AlgebraicGeometry/Seshadri/Lattice/InitialWeights.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.exponentWeight line 13
  2. def OAI.MaximalSeshadri.StrictInitial line 15
  3. def OAI.MaximalSeshadri.LexInitial line 18
  4. lemma OAI.MaximalSeshadri.exponentWeight_nonneg line 23
  5. lemma OAI.MaximalSeshadri.exponentWeight_mono line 26
  6. lemma OAI.MaximalSeshadri.continuous_exponentWeight line 31
  7. lemma OAI.MaximalSeshadri.finite_boundedWeight line 35
  8. lemma OAI.MaximalSeshadri.LexInitial.beta_lt_of_eq_weight line 48
  9. theorem OAI.MaximalSeshadri.exists_strictWeight_of_lex line 60
  10. def OAI.MaximalSeshadri.lexKey line 112
  11. lemma OAI.MaximalSeshadri.lexKey_le_iff line 115
  12. lemma OAI.MaximalSeshadri.lexKey_injective line 120
  13. lemma OAI.MaximalSeshadri.LexInitial.key_le line 130
  14. lemma OAI.MaximalSeshadri.LexInitial.unique line 134
  15. theorem OAI.MaximalSeshadri.exists_lexInitial line 138
  16. theorem OAI.MaximalSeshadri.linearIndependent_of_lexInitial line 159
  17. def OAI.MaximalSeshadri.initialExponentSet line 188
  18. theorem OAI.MaximalSeshadri.exists_initial_basis line 191