OAI/SetTheory/PartitionPrinciple/Definability/NatUnionCodes.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.SetRealization.Presentation.graph line 11
  2. theorem OAI.PartitionPilot.SetRealization.Presentation.pair_mem_graph line 14
  3. theorem OAI.PartitionPilot.SetRealization.Presentation.mem_graph line 18
  4. theorem OAI.PartitionPilot.SetRealization.Presentation.graph_isFunc line 29
  5. theorem OAI.PartitionPilot.SetRealization.Presentation.graph_mem_funs line 40
  6. theorem OAI.PartitionPilot.SetRealization.Presentation.graph_rank_lt line 43
  7. def OAI.PartitionPilot.Forcing.FunctionGraphOn line 58
  8. def OAI.PartitionPilot.Forcing.graphRestriction line 61
  9. theorem OAI.PartitionPilot.Forcing.pair_first_mem_doubleUnion line 64
  10. theorem OAI.PartitionPilot.Forcing.pair_second_mem_doubleUnion line 70
  11. theorem OAI.PartitionPilot.Forcing.pair_mem_graphRestriction line 76
  12. theorem OAI.PartitionPilot.Forcing.mem_graphRestriction line 85
  13. theorem OAI.PartitionPilot.Forcing.graphRestriction_subset line 94
  14. theorem OAI.PartitionPilot.Forcing.graphRestriction_restrict line 97
  15. theorem OAI.PartitionPilot.Forcing.graphRestriction_eq_sep line 110
  16. theorem OAI.PartitionPilot.Forcing.graphRestriction_insert_of_not_mem line 123
  17. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.to_isFunc line 139
  18. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.shape line 147
  19. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.total line 153
  20. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.pair_source line 158
  21. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.unique line 162
  22. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.restrict line 167
  23. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.restriction_eq line 178
  24. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.eq_of_agree line 187
  25. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.empty line 202
  26. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.insert line 205
  27. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.successor line 230
  28. theorem OAI.PartitionPilot.Forcing.functionGraphOn_sUnion line 236
  29. def OAI.PartitionPilot.SetRealization.Presentation.reindex line 263
  30. theorem OAI.PartitionPilot.SetRealization.Presentation.reindex_carrier line 272
  31. theorem OAI.PartitionPilot.SetRealization.Presentation.reindex_encode line 274
  32. theorem OAI.PartitionPilot.SetRealization.Presentation.graph_reindex line 276
  33. def OAI.PartitionPilot.Forcing.NatUnionCode line 290
  34. theorem OAI.PartitionPilot.Forcing.NatUnionCode.subset line 295
  35. theorem OAI.PartitionPilot.Forcing.NatUnionCode.constant line 299
  36. theorem OAI.PartitionPilot.Forcing.NatUnionCode.prod_left line 303
  37. theorem OAI.PartitionPilot.Forcing.NatUnionCode.prod line 316
  38. theorem OAI.PartitionPilot.Forcing.NatUnionCode.isFunc line 333
  39. theorem OAI.PartitionPilot.Forcing.NatUnionCode.function_entry_iff line 354