OAI/Topology/ArtinGroups/Complexes/NegativeTwistCapDisjoint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classNegativeTwist_capOn_disjoint line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseWord_capOn_disjoint line 28
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.finiteFamily_upperBound line 38
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ClassTestUpper.mono line 45
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseWord_iterate_testUpper line 51
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseWord_iterate_boundary line 64
7. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.finiteFamily_cap_accessible_of_test_decrement line 74