OAI/SetTheory/PartitionPrinciple/Forcing/GroundUnionSizeWitnesses.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.belowWitnessRelation line 11
2. theorem OAI.PartitionPilot.Forcing.pair_mem_belowWitnessRelation line 15
3. theorem OAI.PartitionPilot.Forcing.belowWitnessRelation_subset line 31
4. def OAI.PartitionPilot.Forcing.BoundedFormula.belowWitnessEntryFormula line 37
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_belowWitnessEntryFormula line 41
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.belowWitnessRelation_mem line 54
7. def OAI.PartitionPilot.Forcing.TransitiveGround.groundBelowWitnesses line 73
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundBelowWitnesses_mem line 76
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundBelow_iff_boundedWitness line 85
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundBelowWitnesses_total_iff line 98
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.uniform_below_witnesses line 115
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.uniform_below_family line 139
13. theorem OAI.PartitionPilot.Forcing.GroundRegular.bound_witnesses line 161
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.uniform_below_common_bound line 183
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.selected_union_embeds_product line 223
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.paired_union_embeds_product line 233
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.regular_union_embeds_product line 253