OAI/SetTheory/PartitionPrinciple/Definability/RationalCodeLaws.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.fractionEquivalence_code line 11
  2. def OAI.PartitionPilot.Forcing.rationalCarrier line 30
  3. theorem OAI.PartitionPilot.Forcing.rationalCarrier_subset line 33
  4. def OAI.PartitionPilot.Forcing.rationalEncode line 36
  5. theorem OAI.PartitionPilot.Forcing.rationalEncode_spec line 41
  6. theorem OAI.PartitionPilot.Forcing.rationalEncode_class line 48
  7. theorem OAI.PartitionPilot.Forcing.rationalEncode_injective line 58
  8. theorem OAI.PartitionPilot.Forcing.rationalEncode_of_canonical line 66
  9. def OAI.PartitionPilot.Forcing.rationalPresentation line 75
  10. def OAI.PartitionPilot.Forcing.rationalLtGraph line 88
  11. theorem OAI.PartitionPilot.Forcing.rationalLtGraph_subset line 91
  12. theorem OAI.PartitionPilot.Forcing.pair_mem_rationalLtGraph line 95
  13. theorem OAI.PartitionPilot.Forcing.rational_denseOrderCode line 119
  14. theorem OAI.PartitionPilot.Forcing.rationalCarrier_nonempty line 149
  15. theorem OAI.PartitionPilot.Forcing.rational_no_endpoints line 153