OAI/GroupTheory/FiniteType/OrderChainsExactInOfDirected.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OrderChains.exactIn_of_directed line 21
2. theorem OAI.OrderChains.lower_filling_many line 44
3. theorem OAI.OrderChains.exactSet_sublevel line 65
4. theorem OAI.OrderChains.constant_of_exact_zero line 86
5. lemma OAI.TwistedBrin.Basis.firstCut_card line 127
6. lemma OAI.TwistedBrin.Basis.firstCut_nonempty line 133
7. lemma OAI.TwistedBrin.Basis.firstCut_rank_bound line 146
8. theorem OAI.TwistedBrin.Basis.properCutInterval_exactIn line 154
9. def OAI.TwistedBrin.Basis.Merge.endpoint line 186
10. lemma OAI.TwistedBrin.Basis.Merge.endpoint_injective line 187
11. structure OAI.TwistedBrin.Basis.Matching line 192
12. def OAI.TwistedBrin.Basis.Matching.Present line 199
13. abbrev OAI.TwistedBrin.Basis.Matching.Rest line 202
14. abbrev OAI.TwistedBrin.Basis.Matching.Roots line 204
15. def OAI.TwistedBrin.Basis.Matching.rootChart line 206
16. lemma OAI.TwistedBrin.Basis.Matching.endpoint_eq line 210
17. lemma OAI.TwistedBrin.Basis.Matching.range_joined line 215
18. lemma OAI.TwistedBrin.Basis.Matching.rootPartition line 221
19. def OAI.TwistedBrin.Basis.Matching.contract line 260
20. lemma OAI.TwistedBrin.Basis.Matching.mem_contract line 264
21. lemma OAI.TwistedBrin.Basis.Matching.contract_cutRefines line 282
22. def OAI.TwistedBrin.Basis.Matching.leafEquiv line 302
23. lemma OAI.TwistedBrin.Basis.Matching.rank_contract line 330
24. lemma OAI.TwistedBrin.Basis.Matching.present_top line 346
25. lemma OAI.TwistedBrin.Basis.Matching.present_mono line 348
26. lemma OAI.TwistedBrin.Basis.Matching.contract_mono line 367
27. lemma OAI.TwistedBrin.Pattern.card_leaves_ge_two line 428
28. lemma OAI.TwistedBrin.Basis.Forest.leaf_root_eq line 445
29. lemma OAI.TwistedBrin.Basis.Forest.lost_leaves_bound line 457