OAI/SetTheory/PartitionPrinciple/Geometry/GroundIndexedClassInclusions.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.equivalenceClassFormula line 14
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_equivalenceClassFormula line 20
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.equivalenceClassesFormula line 41
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_equivalenceClassesFormula line 44
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.equivalenceClassifierEntryFormula line 52
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_equivalenceClassifierEntryFormula line 56
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equivalenceClass_mem line 72
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equivalenceClasses_eq_sep_groundPower line 88
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equivalenceClasses_mem line 100
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equivalenceClassifier_mem line 120
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equivalenceClasses_spec line 148
  12. def OAI.PartitionPilot.Forcing.indexedClassInclusion line 175
  13. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedClassInclusion line 178
  14. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedClassInclusion_of_entry line 188
  15. theorem OAI.PartitionPilot.Forcing.indexedClassInclusion_function line 195
  16. theorem OAI.PartitionPilot.Forcing.indexedClassInclusion_kernel line 209
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedClassInclusion_mem line 221
  18. def OAI.PartitionPilot.Forcing.TransitiveGround.indexedClassInclusions line 231
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_indexedClassInclusions line 234
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedClassInclusions_mem line 247
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedClassInclusions_function line 252
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedClassInclusions_entries line 259