OAI/SetTheory/PartitionPrinciple/Transfinite/GroundCountableFunctionClosure.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.indexedSizeRelation line 14
  2. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedSizeRelation line 19
  3. theorem OAI.PartitionPilot.Forcing.indexedSizeRelation_partial line 32
  4. theorem OAI.PartitionPilot.Forcing.indexedSizeRelation_onto line 53
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedSizeEntryFormula line 74
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedSizeEntryFormula line 81
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedSizeRelation_mem line 97
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_of_partial_surjection line 117
  9. def OAI.PartitionPilot.Forcing.unionSizeRelation line 140
  10. theorem OAI.PartitionPilot.Forcing.pair_mem_unionSizeRelation line 145
  11. theorem OAI.PartitionPilot.Forcing.unionSizeRelation_partial line 158
  12. theorem OAI.PartitionPilot.Forcing.unionSizeRelation_onto line 176
  13. def OAI.PartitionPilot.Forcing.BoundedFormula.unionSizeEntryFormula line 195
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_unionSizeEntryFormula line 201
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.unionSizeRelation_mem line 216
  16. def OAI.PartitionPilot.Forcing.defaultInverse line 243
  17. theorem OAI.PartitionPilot.Forcing.pair_mem_defaultInverse line 247
  18. theorem OAI.PartitionPilot.Forcing.defaultInverse_isFunc line 254
  19. theorem OAI.PartitionPilot.Forcing.defaultInverse_onto line 280
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.defaultInverse_mem line 293
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_enumeration line 310
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundCountable_enumeration line 324
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.enumerated_union_embeds_product line 348
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countable_enumerated_union line 366
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countable_union_of_sequence_graph line 386
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundCountable_family_union line 415
  27. def OAI.PartitionPilot.Forcing.groundSequenceGraph line 448
  28. def OAI.PartitionPilot.Forcing.groundSequenceUnion line 451
  29. theorem OAI.PartitionPilot.Forcing.mem_groundSequenceUnion line 454
  30. theorem OAI.PartitionPilot.Forcing.groundSequenceUnion_extends line 469
  31. def OAI.PartitionPilot.Forcing.InternallyCountablyClosed line 473
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.descending_function_union_partial line 483
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.descending_function_union_mem line 501
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countable_function_lower_bound line 524
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countable_function_internally_closed line 545