OAI/SetTheory/PartitionPrinciple/Transfinite/RecursiveRefinementMapCoherence.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_self_rawline 16 - theorem
OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_graph_selfline 26 - theorem
OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_comp_rawline 51 - theorem
OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrictionFunction_graph_compline 61