OAI/Combinatorics/TwoWayAutomata/RelationBridge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoWayComplementation.CompanionBridge.relationEquiv line 12

   Source documentation

   Exact currying/uncurrying equivalence of the two full relation alphabets.

   def relationEquiv (H : Type*) : BRel H ≃ SetRel H H where
   …

2. theorem OAI.TwoWayComplementation.CompanionBridge.relationProduct_map line 19

   Source documentation

   Both products compose in path order, including the identity for the empty word.

   theorem relationProduct_map {H : Type*} (w : List (BRel H)) :
       relationProduct (w.map (relationEquiv H)) = relationEquiv H w.prod := by
   …

   Mentions: OAI.TwoWayComplementation.relationProduct, OAI.TwoWayComplementation.CompanionBridge.relationEquiv

3. theorem OAI.TwoWayComplementation.CompanionBridge.sourceLanguage_map_iff line 29