OAI/SetTheory/PartitionPrinciple/Forcing/GroundPrincipalSupportZF.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportBasis_fiber_mem line 14
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.basis_mix_mem line 44
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.basis_symmetric_mix line 56
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_principalSupportEntry line 79
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.principalSupportBasis_mem line 90
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.principalFix_code_mem line 118
7. theorem OAI.PartitionPilot.Forcing.Rows.ground_row_common_support line 135
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ZF_from_principalSupports line 173