OAI/SetTheory/PartitionPrinciple/Forcing/GroundSymmetricPowerSet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.codedPowerEntryFormula line 9
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_codedPowerEntryFormula line 22
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.codedPower_mem line 55
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetricEnvelope_mem line 104
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetricCodedPower_mem line 118
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetric_powerSet line 137