OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixRawCoveredAppend.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_later_entry line 20
  2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_oldProfilePreservation line 29
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.preservedMainPrefixCandidates line 83
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_preservedMainPrefixCandidates line 86
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preservedMainPrefixCandidates_mem line 90
  6. def OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.preservedMainPrefixes line 119
  7. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.preservedMainPrefixes_ground line 122
  8. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.mem_preservedMainPrefixes line 133
  9. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.prefix_mem_preservedMainPrefixes line 138
  10. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.exists_preservedPrefix_of_mem line 148
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_initialPreservedPrefixCandidate line 172
  12. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.exists_rankedPreservedUnionPrefix line 213
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.transition_oldProfilePreservation line 268
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FixedTopStage.RankedChronology.transition_preservesOldProfiles line 280
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_rawCoveredPreservedAppendLimit line 297