OAI/Combinatorics/TwoWayAutomata/Transport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoWayComplementation.Diagram.inclusion_of_missing_empty line 12

   Source documentation

   Losing no recurrent class forces componentwise inclusion.

   theorem inclusion_of_missing_empty {m : ℕ} (e z : Diagram m) (he : comp e e = e)
       (hz : z ∈ e.corner) (hmissing : e.missing z = ∅) : (e, z) ∈ inclusion m := by
   …

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

2. theorem OAI.TwoWayComplementation.Diagram.classRectangle_subset line 25
3. theorem OAI.TwoWayComplementation.Diagram.classRectangle_cross line 34
4. theorem OAI.TwoWayComplementation.Diagram.classRectangle_survives line 44
5. theorem OAI.TwoWayComplementation.Diagram.portRelation_covered line 55
6. theorem OAI.TwoWayComplementation.Diagram.classInfluence_cross line 79
7. theorem OAI.TwoWayComplementation.Diagram.classInfluence_subset line 88
8. theorem OAI.TwoWayComplementation.Diagram.transportMarked_card line 103
9. theorem OAI.TwoWayComplementation.Diagram.missing_context_subset_marked line 133
10. theorem OAI.TwoWayComplementation.Diagram.transport line 158

    Source documentation

    One fixed target set covers every admissible replacement.

    theorem transport {m : ℕ} (e d u v : Diagram m)
        (he : comp e e = e) (hd : comp d d = d) (hcontext : comp (comp u e) v = d)
        (J : Set (Bool × Set (Fin m))) (hJ : J ⊆ e.classes) :
        ∃ J' ⊆ d.classes, J'.ncard ≤ 2 * J.ncard ∧
          ∀ z ∈ e.corner, e.missing z ⊆ J → comp (comp u z) v ∈ d.corner →
            d.missing (comp (comp u z) v) ⊆ J' := by
    …

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