OAI/Combinatorics/HoneycombCorridor/Bridges.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.adjacent_exists_slot line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.exists_advance_of_adjacent line 22
  3. theorem OAI.PolynomialVacuumBridge.Corridor.exists_word_of_chain line 34
  4. def OAI.PolynomialVacuumBridge.Corridor.layer line 60

    Distinct definitions of this name: ComparatorChallenges/HoneycombBridgeFiniteness.lean:26 (different declaration text). Qualify references as OAI.PolynomialVacuumBridge.Corridor.layer@path.

  5. structure OAI.PolynomialVacuumBridge.Corridor.BridgePath line 63

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:29 (same declaration text).

  6. def OAI.PolynomialVacuumBridge.Corridor.weight line 71

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:37 (same declaration text).

  7. def OAI.PolynomialVacuumBridge.Corridor.firstLengthWeight line 74

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:40 (same declaration text).

  8. def OAI.PolynomialVacuumBridge.Corridor.bridgeMass line 77

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:43 (same declaration text).

  9. def OAI.PolynomialVacuumBridge.Corridor.bridgeLengthMass line 78
  10. def OAI.PolynomialVacuumBridge.Corridor.bridgeMean line 80
  11. def OAI.PolynomialVacuumBridge.Corridor.InLogCorridor line 82

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:44 (same declaration text).

  12. def OAI.PolynomialVacuumBridge.Corridor.ConfinedBridgePath line 85

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:47 (same declaration text).

  13. def OAI.PolynomialVacuumBridge.Corridor.confinedMass line 87

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:49 (same declaration text).

  14. def OAI.PolynomialVacuumBridge.Corridor.confinedLengthMass line 89
  15. def OAI.PolynomialVacuumBridge.Corridor.confinedMean line 91
  16. def OAI.PolynomialVacuumBridge.Corridor.Subpower line 93
  17. def OAI.PolynomialVacuumBridge.Corridor.FiniteBridgeSums line 98

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:51 (same declaration text).

  18. def OAI.PolynomialVacuumBridge.Corridor.StripMassAndBridgeLength line 106
  19. theorem OAI.PolynomialVacuumBridge.Corridor.layer_boxIndex line 117
  20. theorem OAI.PolynomialVacuumBridge.Corridor.bridge_exists_word line 120
  21. def OAI.PolynomialVacuumBridge.Corridor.bridgeWord line 174
  22. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeWord_trace line 177
  23. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeWord_terminal_layer line 181
  24. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeWord_length line 185
  25. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeWord_injective line 189
  26. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeWord_mem_sourceExits line 197