OAI/SetTheory/PartitionPrinciple/Forcing/GroundMainPrefixLimitActionLaws.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitAct line 16
2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAct_bounds line 22
3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAct_total line 28
4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAct_unique line 37
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAct_at line 64
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAct_monotone line 83
7. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction line 101
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_ground line 105
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_entry line 110
10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_function line 139
11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_at line 149
12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMaps_action_iff line 158
13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMaps_equivariant line 169
14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_rank_lt line 177
15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitMaps_agreement line 182
16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAct_mul line 216
17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_one line 239
18. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitAction_code line 246