OAI/Combinatorics/ThinTrees/Partitions.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.predecessor_dichotomy line 14
  2. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.domain_descendant_partition line 27
  3. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.domain_avoid_partition line 45
  4. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.innerRecord line 58
  5. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.outsideRecord line 60
  6. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.central_conflict line 63
  7. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.central_domain_disjoint line 76
  8. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.protected_same_side line 84
  9. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.central_valid line 101
  10. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.Compatible line 205
  11. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.compatible_symm line 208
  12. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.compatible_self_iff line 211
  13. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.compatible_heredity line 219
  14. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.candidate_ancestor line 226
  15. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.insert_compatible line 239
  16. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.Interior line 258
  17. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.interior_restriction line 263
  18. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.not_interior_ball line 273
  19. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.labeled_empty line 282
  20. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.labeled_subset line 284
  21. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.labeled_pair line 289
  22. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.labeled_union line 296
  23. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.labeled_sets_disjoint line 310
  24. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.restriction line 328
  25. def OAI.StrongThinTree.MultiGraph.Hierarchy.Record.Refines line 331
  26. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.restriction_refines line 334
  27. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.Record.compatible_refinements line 339
  28. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.labeled_replace line 348
  29. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.replacement_credit line 354