OAI/Combinatorics/TwoWayAutomata/Classes.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoWayComplementation.Diagram.corner_comp line 11
2. theorem OAI.TwoWayComplementation.Diagram.corner_pow_succ line 17
3. theorem OAI.TwoWayComplementation.Diagram.nesting_refl line 23
4. theorem OAI.TwoWayComplementation.Diagram.nesting_trans line 26
5. theorem OAI.TwoWayComplementation.Diagram.comp_mono line 39
6. theorem OAI.TwoWayComplementation.Diagram.through_loop_through line 46
7. theorem OAI.TwoWayComplementation.Diagram.recurrence_idempotent line 54

   Source documentation

   Idempotence of the recurrence relation.

   theorem recurrence_idempotent {m : ℕ} (e : Diagram m) (he : comp e e = e)
       (positive : Bool) :
       e.recurrence positive ○ e.recurrence positive = e.recurrence positive := by
   …

   Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp

8. theorem OAI.TwoWayComplementation.Diagram.corner_returns line 69
9. theorem OAI.TwoWayComplementation.Diagram.corner_forward_absorption line 78

   Source documentation

   Positive through-edge absorption in a corner.

   theorem corner_forward_absorption {m : ℕ} (e z : Diagram m) (hz : z ∈ e.corner) :
       e.forward ○ e.loopClosure true ○ z.forward ⊆ z.forward ∧
       z.forward ○ e.loopClosure true ○ e.forward ⊆ z.forward := by
   …

   Mentions: OAI.TwoWayComplementation.Diagram

10. theorem OAI.TwoWayComplementation.Diagram.corner_through_absorption line 94
11. theorem OAI.TwoWayComplementation.Diagram.loopClosure_comp_self line 116
12. theorem OAI.TwoWayComplementation.Diagram.loopClosure_comp line 120
13. theorem OAI.TwoWayComplementation.Diagram.surviving_absorption line 125
14. theorem OAI.TwoWayComplementation.Diagram.recurrence_trans line 144
15. theorem OAI.TwoWayComplementation.Diagram.class_nonempty line 151
16. theorem OAI.TwoWayComplementation.Diagram.class_related line 156
17. theorem OAI.TwoWayComplementation.Diagram.class_eq_of_mem line 164
18. theorem OAI.TwoWayComplementation.Diagram.class_eq_of_common line 175
19. theorem OAI.TwoWayComplementation.Diagram.surviving_loop_iff line 181
20. theorem OAI.TwoWayComplementation.Diagram.not_mem_missing_iff line 190
21. theorem OAI.TwoWayComplementation.Diagram.missing_self line 201
22. theorem OAI.TwoWayComplementation.Diagram.surviving_comp line 206
23. theorem OAI.TwoWayComplementation.Diagram.missing_comp line 234

    Source documentation

    A class can disappear from a product only if it disappears from a factor.

    theorem missing_comp {m : ℕ} (e z w : Diagram m) (he : comp e e = e)
        (hz : z ∈ e.corner) (hw : w ∈ e.corner) :
        e.missing (comp z w) ⊆ e.missing z ∪ e.missing w := by
    …

    Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp

24. theorem OAI.TwoWayComplementation.Diagram.missing_pow_succ line 251
25. theorem OAI.TwoWayComplementation.Diagram.class_count line 261

    Source documentation

    There are at most two signed recurrent classes per boundary label.

    theorem class_count {m : ℕ} (e : Diagram m) : e.classes.ncard ≤ 2 * m := by
    …

    Mentions: OAI.TwoWayComplementation.Diagram

26. theorem OAI.TwoWayComplementation.Diagram.through_comp_recurrence line 272
27. theorem OAI.TwoWayComplementation.Diagram.recurrence_comp_through line 278
28. theorem OAI.TwoWayComplementation.Diagram.rectangle_subset line 284
29. theorem OAI.TwoWayComplementation.Diagram.rectangle_eq_of_related line 290
30. theorem OAI.TwoWayComplementation.Diagram.rectangle_cover line 315

    Source documentation

    The recurrent rectangles cover every through edge, including for an empty boundary.

    theorem rectangle_cover {m : ℕ} (e : Diagram m) (he : comp e e = e)
        {positive : Bool} {u v : Fin m} (huv : (u, v) ∈ e.through positive) :
        ∃ p, (p, p) ∈ e.recurrence positive ∧ (u, v) ∈ e.rectangle positive p := by
    …

    Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp

31. theorem OAI.TwoWayComplementation.Diagram.rectangle_survives line 330