OAI/NumberTheory/OrdinaryCorrelations/HighTrace/MemSupport.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.mem_support line 20
2. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.support_bot line 26
3. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.support_mono line 33
4. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.le_of_support_subset line 38
5. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.eq_of_support_eq line 45
6. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.eq_bot_iff line 50
7. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.support_ssubset line 59
8. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.holds_mono line 65
9. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.holds_bot line 69
10. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.generates_support line 73
11. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.generates_le line 80
12. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.generates_unique line 88
13. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.generates_holds line 92
14. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.rank_mono line 104
15. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.card_le_rank line 113
16. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.minimal_generators line 118
17. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.generated_width line 149
18. lemma OAI.OrdinaryCorrelations.SourceCylinder.Cylinder.rank_width line 159