OAI/SetTheory/PartitionPrinciple/Transfinite/SetRankBounds.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.SetRealization.rank_singleton_ltline 13 - theorem
OAI.PartitionPilot.SetRealization.rank_unorderedPair_ltline 17 - theorem
OAI.PartitionPilot.SetRealization.rank_orderedPair_ltline 22 - theorem
OAI.PartitionPilot.SetRealization.rank_product_ltline 26 - theorem
OAI.PartitionPilot.SetRealization.Presentation.product_rank_ltline 39 - theorem
OAI.PartitionPilot.SetRealization.Presentation.subset_rank_ltline 44