OAI/Topology/ArtinGroups/Complexes/DownClosed.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.DownClosed line 16
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.DownClosed.low_condition line 20
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.DownClosed.high_condition line 27
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowRestriction line 34
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highRestriction line 36
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowInclusion_commute line 40
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highProjection_commute line 60
8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowInclusion line 81
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highProjection line 88
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowerLevelSet line 95
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.levelDownClosed line 98
12. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowerTruncation line 106
13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.upperTruncation line 108
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowerTruncation_minimal line 112
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.upperTruncation_minimal line 115
16. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowConeNormalized line 118
17. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowConePivot line 121
18. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowCone_source_retained line 134
19. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowCone_reduced_eq line 141
20. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowConeReduction line 151