OAI/SetTheory/PartitionPrinciple/Geometry/UniformAtomicEquality.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.collection_witness line 13
  2. def OAI.PartitionPilot.Forcing.SetFormula.transitiveSetFormula line 31
  3. def OAI.PartitionPilot.Forcing.SetFormula.transitiveCoverFormula line 34
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_transitiveSetFormula line 45
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_transitiveCoverFormula line 56
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_transitiveCover line 63
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_pair_transitiveCover line 110
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.EqualityMeaning line 132
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_membershipFormula line 138
  10. def OAI.PartitionPilot.Forcing.TransitiveGround.namesInTransitiveSet line 219
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_transitiveCover_atomicEquality line 225
  12. def OAI.PartitionPilot.Forcing.SetFormula.equalityCertificateFormula line 256
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equalityCertificate_sound line 266
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_equalityState_fixedPoint line 284
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fixedPoint_equalityCertificate line 305
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equality_fixedPoint_iff line 311
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_atomicEquality_certificate line 344
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.forcesEq_iff_exists_certificate line 369
  19. theorem OAI.PartitionPilot.Forcing.SetFormula.map_empty line 394
  20. def OAI.PartitionPilot.Forcing.SetFormula.uniformEqualityFormula line 399
  21. def OAI.PartitionPilot.Forcing.SetFormula.liftedEqualityFormula line 403
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_uniformEqualityFormula line 415
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equalityMeaning_uniform line 438
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.equalityMeaning_lifted line 450