OAI/SetTheory/PartitionPrinciple/Transfinite/GroundExtensionOrdinals.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.Name.rank_eval_le_code_rank line 14
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinalCode_rank_mem line 33
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinal_eval_mem line 87
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_ordinal_mem line 97
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetricExtension_ordinal_mem line 104