OAI/SetTheory/PartitionPrinciple/Definability/CodedEqualityRelations.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.tripleMembershipFormula line 9
2. def OAI.PartitionPilot.Forcing.Name.codedEqualityRelation line 21
3. theorem OAI.PartitionPilot.Forcing.Name.codedEqualityRelation_mono line 24
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_tripleMembershipFormula line 36
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationMeaning_coded line 63
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.coded_postfixed_sound line 76
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.coded_fixed_iff line 84