OAI/Topology/ArtinGroups/Harmonic/Earlier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.NaturalCylinder.earlier line 14
2. lemma OAI.HarmonicArtin.NaturalCylinder.inl_old line 16
3. lemma OAI.HarmonicArtin.NaturalCylinder.inr_not_old line 17
4. lemma OAI.HarmonicArtin.NaturalCylinder.earlier_inr_iff line 21
5. lemma OAI.HarmonicArtin.NaturalCylinder.link_iff line 33
6. def OAI.HarmonicArtin.NaturalCylinder.linkIso line 49
7. def OAI.HarmonicArtin.lowerOldIso line 59
8. def OAI.HarmonicArtin.lowerOldLowerIso line 67
9. theorem OAI.HarmonicArtin.naturalCylinder_lower_contractible line 76
10. theorem OAI.HarmonicArtin.orderWeights_contractible_of_natural_preimages line 117