OAI/SetTheory/PartitionPrinciple/Definability/EquivalenceClassCodes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.equivalenceClass line 10
  2. theorem OAI.PartitionPilot.Forcing.mem_equivalenceClass line 13
  3. theorem OAI.PartitionPilot.Forcing.equivalenceClass_subset line 17
  4. def OAI.PartitionPilot.Forcing.equivalenceClasses line 20
  5. theorem OAI.PartitionPilot.Forcing.mem_equivalenceClasses line 23
  6. theorem OAI.PartitionPilot.Forcing.equivalenceClass_mem line 29
  7. def OAI.PartitionPilot.Forcing.equivalenceClassifier line 33
  8. theorem OAI.PartitionPilot.Forcing.mem_equivalenceClassifier line 37
  9. theorem OAI.PartitionPilot.Forcing.pair_mem_equivalenceClassifier line 45
  10. theorem OAI.PartitionPilot.Forcing.equivalenceClassifier_function line 56
  11. theorem OAI.PartitionPilot.Forcing.equivalenceClassifier_onto line 64
  12. theorem OAI.PartitionPilot.Forcing.EquivalenceRelationCode.class_self line 72
  13. theorem OAI.PartitionPilot.Forcing.EquivalenceRelationCode.class_eq_iff line 76
  14. theorem OAI.PartitionPilot.Forcing.EquivalenceRelationCode.classifier_kernel line 90
  15. theorem OAI.PartitionPilot.Forcing.EquivalenceRelationCode.class_nonempty line 99