OAI/Combinatorics/HoneycombCorridor/Reflection.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.mirrorVertex line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.mirrorSlot line 14
  3. def OAI.PolynomialVacuumBridge.Corridor.mirrorGerm line 16
  4. def OAI.PolynomialVacuumBridge.Corridor.mirrorWord line 17
  5. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorVertex_invol line 19
  6. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorSlot_invol line 23
  7. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorGerm_invol line 26
  8. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorWord_invol line 29
  9. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorVertex_injective line 32
  10. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorWord_injective line 35
  11. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorWord_length line 38
  12. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_position line 41
  13. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_neighbor line 44
  14. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_advance line 48
  15. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_terminal line 55
  16. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_traced line 63
  17. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_bottomSource line 72
  18. def OAI.PolynomialVacuumBridge.Corridor.mirrorDomain line 74
  19. theorem OAI.PolynomialVacuumBridge.Corridor.mem_mirrorDomain line 76
  20. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorDomain_invol line 85
  21. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_indices line 89
  22. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorDomain_convex line 95
  23. theorem OAI.PolynomialVacuumBridge.Corridor.mirrorDomain_strip line 126
  24. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_sourceExits line 132
  25. theorem OAI.PolynomialVacuumBridge.Corridor.mirror_sourceExits_eq line 149