OAI/Combinatorics/Automata/Diagram.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OneWayLiveness.FiniteWiring.color_eq_of_reachable_from line 11

   Source documentation

   Only edge constraints in the starting component are needed.

   lemma color_eq_of_reachable_from (color : V → C) (s : V)
       (hc : ∀ x y, G.Reachable s x → G.Adj x y → color x = color y)
       {y : V} (h : G.Reachable s y) : color s = color y := by
   …

2. def OAI.OneWayLiveness.Pairing.marked line 28

   Source documentation

   Index the outer identity paths touched by a specified set of interface edges. The definition is made once, independently of a replacement diagram.

   noncomputable def marked (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (J : Finset B) : Finset A :=
   …

   Mentions: OAI.OneWayLiveness.Pairing

3. lemma OAI.OneWayLiveness.Pairing.mem_marked line 32
4. lemma OAI.OneWayLiveness.Pairing.left_reachable_eq line 36
5. lemma OAI.OneWayLiveness.Pairing.marked_card_le line 45
6. lemma OAI.OneWayLiveness.Pairing.support_sandwich_subset_marked line 64

   Source documentation

   Unmarked original identity paths retain their equality constraints through every supported perturbation of the middle diagram.

   lemma support_sandwich_subset_marked (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A))
       (huv : compose v u = identity A) (J : Finset B) (a : Pairing (B ⊕ B))
       (ha : support a ⊆ J) : support (compose (compose v a) u) ⊆ marked v u J := by
   …

   Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.Pairing.compose, OAI.OneWayLiveness.Pairing.identity, OAI.OneWayLiveness.Pairing.support, OAI.OneWayLiveness.Pairing.marked

7. lemma OAI.OneWayLiveness.Pairing.common_support line 120

   Source documentation

   The simultaneous support estimate: a single small set works for every middle diagram supported in the original set, including products and powers.

   lemma common_support (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A))
       (huv : compose v u = identity A) (J : Finset B) :
       ∃ K : Finset A, K.card ≤ J.card ∧ ∀ a : Pairing (B ⊕ B), support a ⊆ J →
         support (compose (compose v a) u) ⊆ K :=
   …

   Mentions: OAI.OneWayLiveness.Pairing, OAI.OneWayLiveness.Pairing.compose, OAI.OneWayLiveness.Pairing.identity, OAI.OneWayLiveness.Pairing.support

8. instance OAI.OneWayLiveness.Pairing.(instance at line 131) line 131
9. lemma OAI.OneWayLiveness.Pairing.mul_eq_compose line 138
10. lemma OAI.OneWayLiveness.Pairing.one_eq_identity line 139
11. lemma OAI.OneWayLiveness.Pairing.rank_one line 141
12. lemma OAI.OneWayLiveness.Pairing.support_one line 149
13. lemma OAI.OneWayLiveness.Pairing.rank_mul_le_left line 153
14. lemma OAI.OneWayLiveness.Pairing.rank_mul_le_right line 155
15. lemma OAI.OneWayLiveness.Pairing.full_rank_isUnit line 158
16. lemma OAI.OneWayLiveness.Pairing.rank_eq_card_of_isUnit line 172
17. lemma OAI.OneWayLiveness.Pairing.rank_mul_unit line 179
18. lemma OAI.OneWayLiveness.Pairing.rank_unit_mul line 184
19. lemma OAI.OneWayLiveness.Pairing.support_mul_subset line 190
20. lemma OAI.OneWayLiveness.Pairing.support_pow_subset line 193
21. def OAI.OneWayLiveness.Pairing.reduce line 202

    Source documentation

    Delete the prescribed caps of an idempotent. Its retained left endpoints are used as the smaller index set, avoiding an arbitrary numbering.

    noncomputable def reduce (e z : Pairing (A ⊕ A)) :
        Pairing ({i // i ∈ lefts e} ⊕ {i // i ∈ lefts e}) :=
    …

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

22. def OAI.OneWayLiveness.Pairing.expand line 206
23. lemma OAI.OneWayLiveness.Pairing.expand_reduce line 210
24. lemma OAI.OneWayLiveness.Pairing.reduce_expand line 213
25. lemma OAI.OneWayLiveness.Pairing.splitRight_absorb line 220
26. lemma OAI.OneWayLiveness.Pairing.splitLeft_absorb line 227
27. lemma OAI.OneWayLiveness.Pairing.reduce_self line 234
28. lemma OAI.OneWayLiveness.Pairing.reduce_mul line 239
29. lemma OAI.OneWayLiveness.Pairing.reduce_sandwich line 245
30. lemma OAI.OneWayLiveness.Pairing.rank_reduce line 252
31. lemma OAI.OneWayLiveness.Pairing.reduce_injective line 262
32. lemma OAI.OneWayLiveness.Pairing.reduce_common_support line 268
33. lemma OAI.OneWayLiveness.Pairing.card_reduced line 277