OAI/Combinatorics/SumProduct/Alignment/RationalLattice21.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.RationalLattice.CoveredLattice line 23
2. lemma OAI.RationalLattice.CoveredLattice.conjugate_le line 32
3. lemma OAI.RationalLattice.CoveredLattice.conjugate_discrete line 36
4. lemma OAI.RationalLattice.CoveredLattice.conjugate_quotient_t2 line 42
5. lemma OAI.RationalLattice.CoveredLattice.conjugate_induced_discrete line 53
6. lemma OAI.RationalLattice.PolynomialArrays.covered_geometry line 81
7. lemma OAI.RationalLattice.PolynomialArrays.filtration_top line 90
8. lemma OAI.RationalLattice.PolynomialArrays.filtration_terminal line 97
9. lemma OAI.RationalLattice.grid_integer_cover line 122
10. lemma OAI.RationalLattice.grid_adapted_cover line 152
11. def OAI.RationalLattice.FiniteProducts.lattice line 192
12. def OAI.RationalLattice.FiniteProducts.projection line 198
13. lemma OAI.RationalLattice.FiniteProducts.projection_continuous line 203
14. lemma OAI.RationalLattice.FiniteProducts.lattice_discrete line 208
15. lemma OAI.RationalLattice.FiniteProducts.grid_lattice line 221
16. lemma OAI.RationalLattice.FiniteProducts.covered_geometry line 245
17. lemma OAI.RationalLattice.FiniteProducts.lattice_compactSpace line 256
18. lemma OAI.RationalLattice.FiniteProducts.filtration_top line 266
19. lemma OAI.RationalLattice.FiniteProducts.filtration_terminal line 273