OAI/SetTheory/PartitionPrinciple/Definability/BoundedAtomicEquality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.orderedTripleFormula line 10
2. def OAI.PartitionPilot.Forcing.SetFormula.codedRelationFormula line 14
3. def OAI.PartitionPilot.Forcing.SetFormula.equalityStateFormula line 16
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_orderedTripleFormula line 29
5. def OAI.PartitionPilot.Forcing.TransitiveGround.equalityParameters line 56
6. def OAI.PartitionPilot.Forcing.TransitiveGround.RawCodedRelation line 59
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawRelationMeaning_coded line 62
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_equalityState line 71
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equalityState_mono line 102
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawEqualityStep_names line 124
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_equalityState_names line 143
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_bounded_atomicEquality line 168