OAI/Combinatorics/Chromatic/Walls/TensorFiltrationInterchange.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.LinearDetection.additiveTensorFiltration_antitone line 14
2. lemma OAI.ElementaryPositivity.LinearDetection.tensor_map_mem_filtration line 21
3. lemma OAI.ElementaryPositivity.LinearDetection.interchange_mem_filtration line 36
4. lemma OAI.ElementaryPositivity.LinearDetection.lift_mem_filtration line 64
5. def OAI.ElementaryPositivity.LinearFiltration.next line 83
6. def OAI.ElementaryPositivity.LinearFiltration.Grade line 84
7. instance OAI.ElementaryPositivity.LinearFiltration.(instance at line 85) line 85
8. instance OAI.ElementaryPositivity.LinearFiltration.(instance at line 87) line 87
9. def OAI.ElementaryPositivity.LinearFiltration.mk line 89
10. def OAI.ElementaryPositivity.LinearFiltration.restrict line 90
11. def OAI.ElementaryPositivity.LinearFiltration.map line 93
12. lemma OAI.ElementaryPositivity.LinearFiltration.map_mk line 99
13. lemma OAI.ElementaryPositivity.LinearFiltration.map_eq_zero line 103
14. lemma OAI.ElementaryPositivity.LinearDetection.assoc_mem_tensorFiltration line 122
15. lemma OAI.ElementaryPositivity.LinearDetection.unassoc_mem_tensorFiltration line 145