OAI/Combinatorics/TwoWayAutomata/Relations.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoWayComplementation.relStar_mono line 10
2. theorem OAI.TwoWayComplementation.relStar_empty line 15
3. theorem OAI.TwoWayComplementation.relStar_comp_self line 26
4. def OAI.TwoWayComplementation.blockRelation line 33

   Source documentation

   A directed graph partitioned into two kinds of vertices.

   def blockRelation {α β : Type*} (E : SetRel α α) (F : SetRel α β)
       (G : SetRel β α) (H : SetRel β β) : SetRel (α ⊕ β) (α ⊕ β) :=
   …

5. theorem OAI.TwoWayComplementation.blockRelation_star_right line 42

   Source documentation

   Eliminate the left block by replacing each finite excursion with one edge.

   theorem blockRelation_star_right {α β : Type*} (E : SetRel α α) (F : SetRel α β)
       (G : SetRel β α) (H : SetRel β β) (x y : β) :
       ((Sum.inr x), (Sum.inr y)) ∈ relStar (blockRelation E F G H) ↔
         (x, y) ∈ relStar (H ∪ (G ○ relStar E ○ F)) := by
   …

   Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.blockRelation

6. theorem OAI.TwoWayComplementation.blockRelation_star_cross line 78

   Source documentation

   A path from the left block first leaves it once, then makes arbitrary finite excursions.

   theorem blockRelation_star_cross {α β : Type*} (E : SetRel α α) (F : SetRel α β)
       (G : SetRel β α) (H : SetRel β β) (x : α) (y : β) :
       ((Sum.inl x), (Sum.inr y)) ∈ relStar (blockRelation E F G H) ↔
         (x, y) ∈ relStar E ○ F ○ relStar (H ∪ (G ○ relStar E ○ F)) := by
   …

   Mentions: OAI.TwoWayComplementation.relStar, OAI.TwoWayComplementation.blockRelation

7. theorem OAI.TwoWayComplementation.relStar_union line 107

   Source documentation

   Closure of a union factors into alternating finite paths.

   theorem relStar_union {α : Type*} (A B : SetRel α α) :
       relStar (A ∪ B) = relStar A ○ relStar (B ○ relStar A) := by
   …

   Mentions: OAI.TwoWayComplementation.relStar

8. theorem OAI.TwoWayComplementation.comp_relStar_rotate line 126

   Source documentation

   A finite alternating path can be rotated between its endpoint types.

   theorem comp_relStar_rotate {α β : Type*} (A : SetRel α β) (B : SetRel β α) :
       A ○ relStar (B ○ A) = relStar (A ○ B) ○ A := by
   …

   Mentions: OAI.TwoWayComplementation.relStar

9. theorem OAI.TwoWayComplementation.relComp_union line 145
10. theorem OAI.TwoWayComplementation.union_relComp line 151
11. theorem OAI.TwoWayComplementation.relStar_unfold line 157
12. theorem OAI.TwoWayComplementation.relStar_block_forward line 171

    Source documentation

    Eliminating two internal boundaries in either order gives the same through relation.

    theorem relStar_block_forward {α : Type*} (A B C D : SetRel α α) :
        relStar (A ∪ (B ○ relStar D ○ C)) ○ B ○ relStar D =
          relStar A ○ B ○ relStar (D ∪ (C ○ relStar A ○ B)) := by
    …

    Mentions: OAI.TwoWayComplementation.relStar

13. theorem OAI.TwoWayComplementation.relStar_block_return line 179

    Source documentation

    The corresponding return relation when eliminating two internal boundaries.

    theorem relStar_block_return {α : Type*} (A B C D : SetRel α α) :
        relStar (A ∪ (B ○ relStar D ○ C)) =
          relStar A ∪ (relStar A ○ B ○ relStar (D ∪ (C ○ relStar A ○ B)) ○
            C ○ relStar A) := by
    …

    Mentions: OAI.TwoWayComplementation.relStar

14. theorem OAI.TwoWayComplementation.relStar_comp_unfold line 191
15. theorem OAI.TwoWayComplementation.relStar_block_exit line 197
16. theorem OAI.TwoWayComplementation.relStar_lost_edge line 221

    Source documentation

    A path lost after an edge replacement contains a lost edge between old path segments.

    theorem relStar_lost_edge {α : Type*} (R S : SetRel α α) {x y : α}
        (hxy : (x, y) ∈ relStar R) (hnot : (x, y) ∉ relStar S) :
        ∃ a b, (x, a) ∈ relStar R ∧ (a, b) ∈ R ∧ (a, b) ∉ S ∧ (b, y) ∈ relStar R := by
    …

    Mentions: OAI.TwoWayComplementation.relStar

17. theorem OAI.TwoWayComplementation.feedback_lost_edge line 235

    Source documentation

    A lost alternating traversal has a lost edge, allowing earlier and later bounces.

    theorem feedback_lost_edge {α : Type*} (E E' B : SetRel α α) {x y : α}
        (hxy : (x, y) ∈ E ○ relStar (B ○ E))
        (hnot : (x, y) ∉ E' ○ relStar (B ○ E')) :
        ∃ a b, (x, a) ∈ relStar (E ○ B) ∧ (a, b) ∈ E ∧
          (a, b) ∉ E' ∧ (b, y) ∈ relStar (B ○ E) := by
    …

    Mentions: OAI.TwoWayComplementation.relStar

18. theorem OAI.TwoWayComplementation.feedback_insert line 253
19. theorem OAI.TwoWayComplementation.weighted_class_bound line 258

    Source documentation

    A bound for weighted classes with integer weights one and two.

    theorem weighted_class_bound {α β : Type*} (X M : Finset α) (Y : Finset β)
        (R : β → α → Prop) (hM : M ⊆ X)
        (hunique : ∀ y ∈ Y, ∀ z ∈ Y, ∀ x ∈ X, R y x → R z x → y = z)
        (hcover : ∀ y ∈ Y,
          (∃ x ∈ X, x ∉ M ∧ R y x) ∨
            ∃ x ∈ X, ∃ z ∈ X, x ≠ z ∧ R y x ∧ R y z) :
        2 * Y.card + M.card ≤ 2 * X.card := by
    …

20. theorem OAI.TwoWayComplementation.idempotent_relation_factor line 318

    Source documentation

    Every edge of a finite idempotent relation factors through a recurrent point.

    theorem idempotent_relation_factor {α : Type*} [Finite α] (P : SetRel α α)
        (hP : P ○ P = P) {u v : α} (huv : (u, v) ∈ P) :
        ∃ p, (u, p) ∈ P ∧ (p, p) ∈ P ∧ (p, v) ∈ P := by
    …