OAI/SetTheory/PartitionPrinciple/Definability/EqualityStepSyntax.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.atomicApplication line 12
2. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_atomicApplication line 16
3. def OAI.PartitionPilot.Forcing.SetFormula.membershipFormula line 22
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_conditionLE line 41
5. def OAI.PartitionPilot.Forcing.TransitiveGround.RelationMeaning line 62
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_relationMembership line 68
7. def OAI.PartitionPilot.Forcing.SetFormula.swapEquality line 146
8. def OAI.PartitionPilot.Forcing.SetFormula.matchingDirectionFormula line 149
9. def OAI.PartitionPilot.Forcing.SetFormula.equalityStepFormula line 158
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationMeaning_swap line 171