OAI/Topology/ArtinGroups/Quivers/ClosedNeighborhood.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.closedNeighborhood line 10
2. lemma OAI.HarmonicArtin.ReversibleQuiver.mem_closedNeighborhood line 13
3. lemma OAI.HarmonicArtin.ReversibleQuiver.corner_target_mem_neighborhood line 16
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ClassCapOn line 31
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ClassCapOn.mono line 36
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classCapOn_of_upper line 40
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.reducedNegativeAmplitudeTwist_cap line 43
8. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classNegativeTwist_capOn line 59
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseWord_capOn line 81