OAI/SetTheory/PartitionPrinciple/Definability/GroundFlatCopyPresentation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.SetRealization.Presentation.quotientEncode line 16
  2. theorem OAI.PartitionPilot.SetRealization.Presentation.quotientEncode_mk line 21
  3. theorem OAI.PartitionPilot.SetRealization.Presentation.quotientEncode_injective line 25
  4. theorem OAI.PartitionPilot.SetRealization.Presentation.mem_equivalenceClasses_iff_quotientEncode line 33
  5. def OAI.PartitionPilot.SetRealization.Presentation.quotientPresentation line 46
  6. theorem OAI.PartitionPilot.SetRealization.Presentation.quotientPresentation_carrier line 52
  7. theorem OAI.PartitionPilot.SetRealization.Presentation.quotientPresentation_encode_mk line 55
  8. theorem OAI.PartitionPilot.SetRealization.Presentation.quotientPresentation_classifier_entry_iff line 59
  9. theorem OAI.PartitionPilot.SetRealization.Presentation.quotientClassifier_eq_graph line 70
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.quotientPresentation_carrier_mem line 95
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.quotientMapGraph_mem line 101
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyEquivalence_code line 130
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_flatCopyEquivalence line 137
  14. def OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyPresentation line 143
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyPresentation_carrier line 149
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyPresentation_encode_copy line 154
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyClassifier_eq_graph line 167
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyPresentation_ground line 184