OAI/Combinatorics/ParityLifts/GlueVertices.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.GlueRootRel line 16
  2. def OAI.ParityWL.GlueRoot line 19
  3. instance OAI.ParityWL.glueRootFintype line 21
  4. abbrev OAI.ParityWL.GlueInternal line 25
  5. abbrev OAI.ParityWL.GlueVertex line 27
  6. def OAI.ParityWL.glueRoot line 31
  7. def OAI.ParityWL.glueMap line 33
  8. lemma OAI.ParityWL.glueMap_root line 37
  9. lemma OAI.ParityWL.glueMap_internal line 46
  10. lemma OAI.ParityWL.glueMap_eq_inl line 50
  11. lemma OAI.ParityWL.glueMap_eq_internal line 56
  12. def OAI.ParityWL.glueBag line 71
  13. lemma OAI.ParityWL.glueBag_root_mem line 75
  14. lemma OAI.ParityWL.glueMap_mem_bag line 80
  15. lemma OAI.ParityWL.glueBag_internal line 92
  16. lemma OAI.ParityWL.glueBag_root_ancestor line 122
  17. lemma OAI.ParityWL.glueBag_internal_same line 134
  18. lemma OAI.ParityWL.internal_top_nonroot line 146
  19. def OAI.ParityWL.glueTop line 153
  20. lemma OAI.ParityWL.glueTop_mem line 157
  21. lemma OAI.ParityWL.glueTop_ancestor line 166
  22. lemma OAI.ParityWL.glueInterval_mem line 176
  23. lemma OAI.ParityWL.glueIntersection_sub line 191
  24. def OAI.ParityWL.glueRelation line 211
  25. lemma OAI.ParityWL.glueRelation_symm line 214
  26. def OAI.ParityWL.glueBagTree line 219
  27. def OAI.ParityWL.glueTest line 248
  28. def OAI.ParityWL.glueValue line 261
  29. lemma OAI.ParityWL.glueValue_root line 270
  30. lemma OAI.ParityWL.glueValue_map line 273
  31. def OAI.ParityWL.glueMapsEquiv line 282
  32. lemma OAI.ParityWL.glueTest_count line 316