OAI/AlgebraicGeometry/Seshadri/Interpolation/QuadrilateralRows.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Interpolation.nodeQuadrilateral line 12
2. def OAI.MaximalSeshadri.Interpolation.rowTriangle line 15
3. theorem OAI.MaximalSeshadri.Interpolation.mem_rowTriangle_of_inequalities line 18
4. theorem OAI.MaximalSeshadri.Interpolation.nodeQuadrilateral_constraints line 52
5. theorem OAI.MaximalSeshadri.Interpolation.diagonal_compress_mem line 80
6. def OAI.MaximalSeshadri.Interpolation.diagonalIndex line 105
7. def OAI.MaximalSeshadri.Interpolation.diagonalRows line 107
8. def OAI.MaximalSeshadri.Interpolation.diagonalRow line 109
9. def OAI.MaximalSeshadri.Interpolation.rowStart line 112
10. def OAI.MaximalSeshadri.Interpolation.rowHeight line 114
11. theorem OAI.MaximalSeshadri.Interpolation.diagonalRow_nonempty line 117
12. theorem OAI.MaximalSeshadri.Interpolation.rowStart_add_min line 122
13. def OAI.MaximalSeshadri.Interpolation.rowEmbedding line 127
14. theorem OAI.MaximalSeshadri.Interpolation.rowEmbedding_second line 135
15. theorem OAI.MaximalSeshadri.Interpolation.rowEmbedding_first line 139
16. theorem OAI.MaximalSeshadri.Interpolation.rowEmbedding_injective line 146
17. theorem OAI.MaximalSeshadri.Interpolation.rowEnvelope_dominated line 158
18. theorem OAI.MaximalSeshadri.Interpolation.compressed_row_exponent_injective line 167
19. theorem OAI.MaximalSeshadri.Interpolation.rowEnvelope_mem_triangle line 181
20. theorem OAI.MaximalSeshadri.Interpolation.quadrilateral_jet_rank_of_triangle_test line 198