OAI/SetTheory/PartitionPrinciple/Definability/GroundPartialFunctionSpaces.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.GroundDefinableFunction line 11
  2. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.projection line 20
  3. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.reindex line 26
  4. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.compFormula line 36
  5. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.comp line 43
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.productElementFormula line 92
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_productElementFormula line 95
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_groundPower line 108
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPower_mem line 112
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.prod_mem line 123
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.groundRelations line 153
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_groundRelations line 155
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundRelations_mem line 158
  14. structure OAI.PartitionPilot.Forcing.PartialFunctionCode line 174
  15. theorem OAI.PartitionPilot.Forcing.PartialFunctionCode.empty line 180
  16. theorem OAI.PartitionPilot.Forcing.PartialFunctionCode.mono line 183
  17. theorem OAI.PartitionPilot.Forcing.PartialFunctionCode.union line 186
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.partialFunctionFormula line 205
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_partialFunctionFormula line 210
  20. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_product line 234
  21. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_groundPower line 249
  22. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_groundRelations line 262
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.familySetEntryFormula line 279
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_familySetEntryFormula line 282
  25. def OAI.PartitionPilot.Forcing.SetFormula.familySetCodeFormula line 301
  26. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_familySetCode line 309
  27. def OAI.PartitionPilot.Forcing.TransitiveGround.partialFunctions line 337
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_partialFunctions line 340
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.partialFunctions_mem line 345
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.empty_mem_partialFunctions line 374
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.partialFunctions_restrict line 378
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.partialFunctions_union line 382