OAI/Combinatorics/Automata/Relations.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OneWayLiveness.BRel.restrictedId_holds line 10
  2. lemma OAI.OneWayLiveness.BRel.restrictedId_idem line 12
  3. lemma OAI.OneWayLiveness.BRel.restrictedId_mul line 15
  4. lemma OAI.OneWayLiveness.BRel.mul_restrictedId line 17
  5. lemma OAI.OneWayLiveness.BRel.corner_supported line 20
  6. def OAI.OneWayLiveness.BRel.restriction line 28
  7. def OAI.OneWayLiveness.BRel.extend line 41
  8. def OAI.OneWayLiveness.BRel.extension line 44
  9. def OAI.OneWayLiveness.BRel.restrictionEquiv line 48
  10. lemma OAI.OneWayLiveness.BRel.relation_corner line 64

    Source documentation

    Restrict a relation corner with a split subidentity.

    lemma relation_corner {P : BRel H} (hP : P * P = P) (F : Set H)
    (hF : restrictedId F * P * restrictedId F = restrictedId F) :
    let Q := P * restrictedId F * P
…

    Mentions: OAI.OneWayLiveness.BRel, OAI.OneWayLiveness.BRel.restrictedId

  11. def OAI.OneWayLiveness.BRel.permGraph line 103
  12. lemma OAI.OneWayLiveness.BRel.permGraph_holds line 104
  13. def OAI.OneWayLiveness.BRel.permUnit line 107
  14. def OAI.OneWayLiveness.BRel.addEdge line 114

    Source documentation

    The identity with one extra pair.

    def addEdge (x y : H) : BRel H := ⟨fun u v => u = v ∨ u = x ∧ v = y⟩

    Mentions: OAI.OneWayLiveness.BRel

  15. lemma OAI.OneWayLiveness.BRel.addEdge_holds line 115
  16. lemma OAI.OneWayLiveness.BRel.addEdge_idem line 117
  17. lemma OAI.OneWayLiveness.BRel.addEdge_ne_one line 121
  18. lemma OAI.OneWayLiveness.BRel.conjugate_addEdge line 127
  19. lemma OAI.OneWayLiveness.BRel.exists_perm_pair line 142
  20. def OAI.OneWayLiveness.HasUnitLifts line 157

    Source documentation

    Every target unit admits a unit lift (unitality included in the homomorphism).

    def HasUnitLifts {M N : Type*} [Monoid M] [Monoid N] (f : M →* N) : Prop :=
…
  21. lemma OAI.OneWayLiveness.unit_image_inv line 160
  22. lemma OAI.OneWayLiveness.conjugate_lift line 165
  23. structure OAI.OneWayLiveness.RectangleFrame line 183

    Source documentation

    Disjoint source/target points and a separate intermediate hub.

    structure RectangleFrame (H I J : Type*) where
…
  24. def OAI.OneWayLiveness.RectangleFrame.base line 195
  25. def OAI.OneWayLiveness.RectangleFrame.rel line 196
  26. lemma OAI.OneWayLiveness.RectangleFrame.rel_holds line 199
  27. lemma OAI.OneWayLiveness.RectangleFrame.rel_empty line 201
  28. lemma OAI.OneWayLiveness.RectangleFrame.rel_mul line 203
  29. lemma OAI.OneWayLiveness.RectangleFrame.rel_idem line 221
  30. lemma OAI.OneWayLiveness.RectangleFrame.rel_absorb line 223
  31. lemma OAI.OneWayLiveness.RectangleFrame.generator_image line 228
  32. lemma OAI.OneWayLiveness.RectangleFrame.restricted_old line 242
  33. lemma OAI.OneWayLiveness.RectangleFrame.restricted_new line 255
  34. def OAI.OneWayLiveness.Corner.flattenEquiv line 278
  35. lemma OAI.OneWayLiveness.HasUnitLifts.comp_equiv line 295
  36. lemma OAI.OneWayLiveness.min_rank_corner_unitLifts line 304
  37. lemma OAI.OneWayLiveness.BRel.restricted_sandwich line 318
  38. lemma OAI.OneWayLiveness.BRel.sandwich_holds_on line 333