OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixConeValues.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundMainPrefix.pointCone line 16
2. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorCone line 23
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointCone_kernel line 30
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorCone_kernel line 36
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitCoverage.point_quotient_bijection line 46
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitCoverage.actor_quotient_bijection line 60
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_order_iff line 71
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_map_meet line 83
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_meetEmbedding line 96
10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_meet_iff line 104
11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorConeMap_mul line 126
12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorConeMap_groupEmbedding line 139
13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorConeMap_inv line 148
14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.coneMaps_equivariant line 158
15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_bottom line 170
16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_height line 176
17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointConeMap_birth line 182