OAI/SetTheory/PartitionPrinciple/Definability/NaturalSetCodes.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.SetRealization.SetMembers line 11
  2. def OAI.PartitionPilot.SetRealization.SetMembers.raw line 15
  3. theorem OAI.PartitionPilot.SetRealization.SetMembers.raw_mem line 18
  4. theorem OAI.PartitionPilot.SetRealization.SetMembers.raw_injective line 21
  5. def OAI.PartitionPilot.SetRealization.SetMembers.ofMem line 26
  6. theorem OAI.PartitionPilot.SetRealization.SetMembers.raw_ofMem line 29
  7. theorem OAI.PartitionPilot.SetRealization.SetMembers.ofMem_raw line 32
  8. def OAI.PartitionPilot.SetRealization.SetMembers.presentation line 35
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.setMember_ground line 52
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.setMembers_countable line 55
  11. def OAI.PartitionPilot.Forcing.natSetCode line 66
  12. theorem OAI.PartitionPilot.Forcing.natSetCode_zero line 68
  13. theorem OAI.PartitionPilot.Forcing.natSetCode_succ line 70
  14. theorem OAI.PartitionPilot.Forcing.mem_omega_iff_natSetCode line 73
  15. theorem OAI.PartitionPilot.Forcing.natSetCode_mem_omega line 83
  16. def OAI.PartitionPilot.Forcing.zeroOrSuccessor line 86
  17. def OAI.PartitionPilot.Forcing.naturalSetProperty line 89
  18. theorem OAI.PartitionPilot.Forcing.naturalSetProperty_empty line 93
  19. theorem OAI.PartitionPilot.Forcing.naturalSetProperty_succ line 100
  20. theorem OAI.PartitionPilot.Forcing.naturalSetProperty_member line 112
  21. theorem OAI.PartitionPilot.Forcing.naturalSetProperty_iff line 117
  22. theorem OAI.PartitionPilot.Forcing.naturalSetProperty_iff_mem_omega line 132
  23. instance OAI.PartitionPilot.Forcing.omegaMembers_countable line 136