OAI/Topology/ArtinGroups/Harmonic/EarlierLower.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.SourceEarlierLower line 10
2. def OAI.HarmonicArtin.sourceEligibleSet line 12
3. lemma OAI.HarmonicArtin.sourceEligible_shared line 14
4. def OAI.HarmonicArtin.sourceLowerClose line 22
5. lemma OAI.HarmonicArtin.le_sourceLowerClose line 26
6. lemma OAI.HarmonicArtin.sourceLowerClose_le line 32
7. lemma OAI.HarmonicArtin.sourceLowerClose_all_eligible line 39
8. lemma OAI.HarmonicArtin.sourceLowerClose_mem line 47
9. lemma OAI.HarmonicArtin.sourceLowerClose_monotone line 58
10. def OAI.HarmonicArtin.sourceLowerRetraction line 71
11. lemma OAI.HarmonicArtin.le_sourceLowerRetraction line 76
12. lemma OAI.HarmonicArtin.sourceLowerClose_eq_of_all line 79
13. lemma OAI.HarmonicArtin.sourceLowerRetraction_idem line 92