OAI/Combinatorics/HoneycombBridges/Factorization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Unique irreducible factorization of strict bridges.

  1. def OAI.HoneycombActual.bridgeProduct line 14
  2. theorem OAI.HoneycombActual.bridgeProduct_nil line 20
  3. theorem OAI.HoneycombActual.bridgeProduct_singleton line 21
  4. theorem OAI.HoneycombActual.bridgeProduct_eq_none_iff line 23
  5. theorem OAI.HoneycombActual.bridgeProduct_exists_of_ne_nil line 27
  6. theorem OAI.HoneycombActual.bridgeProduct_vertices line 33
  7. theorem OAI.HoneycombActual.bridgeProduct_of_vertices line 50
  8. theorem OAI.HoneycombActual.bridgeProduct_append line 60
  9. theorem OAI.HoneycombActual.irreducible_factorization_exists line 78
  10. theorem OAI.HoneycombActual.Bridge.concat_not_irreducible line 102
  11. theorem OAI.HoneycombActual.irreducible_product_unique line 107
  12. theorem OAI.HoneycombActual.bridgeFactorization line 153