OAI/Topology/ArtinGroups/Complexes/TargetLow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.targetLow line 15
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.targetLow_inclusion line 22
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.targetLow_homSpace line 34
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.targetLow_differential line 41
5. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.low_boundary_of_inclusion_boundary line 63
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowerTruncation_homDimension_zero line 83
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLowerTruncation_homDimension_zero line 95