OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainFinalChronology.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.GroundMainPrefix.finalGeometryline 18 - structure
OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalChronologyline 67 - theorem
OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_finalChronologyline 80 - theorem
OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalChronology.code_groundline 94 - theorem
OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalChronology.history_valuesline 96 - theorem
OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalChronology.terminal_valuesline 105 - theorem
OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalChronology.earlier_valuesline 116 - theorem
OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalChronology.earlier_entriesline 130