OAI/SetTheory/PartitionPrinciple/Geometry/GroundNaturalFamilyShift.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.heightColumnFiber line 12
  2. def OAI.PartitionPilot.Forcing.heightColumnGraph line 15
  3. theorem OAI.PartitionPilot.Forcing.mem_heightColumnFiber line 18
  4. theorem OAI.PartitionPilot.Forcing.pair_mem_heightColumnGraph line 34
  5. theorem OAI.PartitionPilot.Forcing.heightColumnGraph_injection line 49
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.heightColumnFiber_mem line 77
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.heightColumnGraph_mem line 91
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_heightColumnFiber line 104
  9. theorem OAI.PartitionPilot.Forcing.ordinalSetProperty_mem_compare line 130
  10. theorem OAI.PartitionPilot.Forcing.ordinalSubset_has_least line 140
  11. def OAI.PartitionPilot.Forcing.ordinalIndexTail line 151
  12. theorem OAI.PartitionPilot.Forcing.mem_ordinalIndexTail line 154
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinalIndexTail_mem line 162
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundCountable_descending_heights line 170
  15. def OAI.PartitionPilot.Forcing.EssentialHeightDescent line 256
  16. theorem OAI.PartitionPilot.Forcing.relationCompose_function_of_subset line 262
  17. theorem OAI.PartitionPilot.Forcing.essentialHeightComposite_strict line 276
  18. theorem OAI.PartitionPilot.Forcing.essentialHeightComposite_antitone line 289
  19. theorem OAI.PartitionPilot.Forcing.essentialHeightComposite_injection line 300
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_essentialBirthHeights line 335
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.essentialBirthIndices_countable line 372
  22. def OAI.PartitionPilot.Forcing.naturalFamilyShift line 403
  23. theorem OAI.PartitionPilot.Forcing.naturalFamilyShift_entries line 406
  24. theorem OAI.PartitionPilot.Forcing.naturalFamilyShift_function line 419
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.naturalFamilyShift_mem line 432