OAI/SetTheory/PartitionPrinciple/Models/GroundSupportedEqualityChoices.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.OrdinalChoiceValue line 13
  2. def OAI.PartitionPilot.Forcing.ordinalIndexedChoiceGraph line 16
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_ordinalIndexedChoiceGraph line 20
  4. theorem OAI.PartitionPilot.Forcing.ordinalIndexedChoiceGraph_choice line 32
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.ordinalChoiceValueFormula line 63
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ordinalChoiceValueFormula line 67
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.ordinalIndexedChoiceEntryFormula line 73
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ordinalIndexedChoiceEntryFormula line 77
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinalIndexedChoiceGraph_mem line 89
  10. theorem OAI.PartitionPilot.Forcing.ordinalIndexedChoiceGraph_total line 116
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ordinalRelationChoice line 134
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.choice_of_witnesses line 170
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_choice_witness line 200
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryExtension_choice line 244
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedNameFamily_graph_choice line 259
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ground_supportedEqualityChoice line 357