OAI/Combinatorics/Automata/Rank.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OneWayLiveness.Pairing.identity_link line 11
2. lemma OAI.OneWayLiveness.Pairing.eq_identity line 15
3. lemma OAI.OneWayLiveness.Pairing.compose_link_iff line 29
4. lemma OAI.OneWayLiveness.Pairing.compose_left_cap line 32
5. lemma OAI.OneWayLiveness.Pairing.compose_right_cap line 42
6. lemma OAI.OneWayLiveness.Pairing.compose_transversal line 52
7. def OAI.OneWayLiveness.Pairing.lefts line 60
8. def OAI.OneWayLiveness.Pairing.rights line 62
9. def OAI.OneWayLiveness.Pairing.rank line 64
10. lemma OAI.OneWayLiveness.Pairing.mem_lefts line 66
11. lemma OAI.OneWayLiveness.Pairing.mem_rights line 68
12. def OAI.OneWayLiveness.Pairing.transversalEquiv line 72

    Source documentation

    The matching bijects its left and right transversal endpoints.

    noncomputable def transversalEquiv (a : Pairing (A ⊕ B)) :
        {i // i ∈ lefts a} ≃ {j // j ∈ rights a} := by
    …

    Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.Pairing.lefts, OAI.OneWayLiveness.Pairing.rights

13. lemma OAI.OneWayLiveness.Pairing.rank_eq_rights line 92
14. lemma OAI.OneWayLiveness.Pairing.lefts_compose_subset line 95
15. lemma OAI.OneWayLiveness.Pairing.rights_compose_subset line 106
16. lemma OAI.OneWayLiveness.Pairing.rank_compose_le_left line 118
17. lemma OAI.OneWayLiveness.Pairing.rank_compose_le_right line 120
18. lemma OAI.OneWayLiveness.Pairing.rank_le_card line 124
19. def OAI.OneWayLiveness.Pairing.support line 127
20. lemma OAI.OneWayLiveness.Pairing.mem_support line 129
21. lemma OAI.OneWayLiveness.Pairing.defect_le_support line 132
22. lemma OAI.OneWayLiveness.Pairing.support_compose_subset line 143
23. lemma OAI.OneWayLiveness.Pairing.support_idempotent_subset line 153
24. lemma OAI.OneWayLiveness.Pairing.support_idempotent_bound line 167
25. lemma OAI.OneWayLiveness.Pairing.idempotent_full_rank line 179
26. lemma OAI.OneWayLiveness.Pairing.eq_of_link_imp line 196
27. def OAI.OneWayLiveness.Pairing.flip line 206
28. lemma OAI.OneWayLiveness.Pairing.flip_link line 208
29. lemma OAI.OneWayLiveness.Pairing.flip_flip line 211
30. lemma OAI.OneWayLiveness.Pairing.left_cap_not_lefts line 217
31. lemma OAI.OneWayLiveness.Pairing.right_cap_not_rights line 224
32. lemma OAI.OneWayLiveness.Pairing.compose_flip_eq_identity line 231
33. lemma OAI.OneWayLiveness.Pairing.compose_cancel_left line 238
34. lemma OAI.OneWayLiveness.Pairing.compose_cancel_right line 244
35. def OAI.OneWayLiveness.Pairing.splitLeft line 251

    Source documentation

    Retain the left caps and straighten the left transversal endpoints.

    noncomputable def splitLeft (e : Pairing (A ⊕ A)) : Pairing (A ⊕ {i // i ∈ lefts e}) where
    …

    Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.Pairing.lefts

36. def OAI.OneWayLiveness.Pairing.splitRight line 295

    Source documentation

    Retain the right caps and all the original transversals.

    noncomputable def splitRight (e : Pairing (A ⊕ A)) : Pairing ({i // i ∈ lefts e} ⊕ A) where
    …

    Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.Pairing.lefts

37. lemma OAI.OneWayLiveness.Pairing.splitLeft_splitRight line 337
38. lemma OAI.OneWayLiveness.Pairing.splitLeft_inverse line 351
39. lemma OAI.OneWayLiveness.Pairing.splitRight_inverse line 359
40. lemma OAI.OneWayLiveness.Pairing.splitRight_splitLeft line 366