OAI/SetTheory/PartitionPrinciple/Forcing/ConditionQuantifiers.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.grandchildrenBound line 14
  2. theorem OAI.PartitionPilot.Forcing.Name.grandchild_mem_bound line 16
  3. theorem OAI.PartitionPilot.Forcing.Name.isName_of_pair_mem line 28
  4. theorem OAI.PartitionPilot.Forcing.Name.unionName_subset_bound line 34
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.grandchildrenBound_mem line 50
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_unionName_bound line 54
  7. def OAI.PartitionPilot.SetRealization.Presentation.conditionOrder line 73
  8. theorem OAI.PartitionPilot.SetRealization.Presentation.pair_mem_conditionOrder line 75
  9. def OAI.PartitionPilot.Forcing.Name.unionEntryParams line 87
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.unionEntryParams_mem line 98
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.unionEntry_iff_mem line 106
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.unionName_mem line 142
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetric_union line 174
  14. def OAI.PartitionPilot.Forcing.SetFormula.allConditions line 192
  15. def OAI.PartitionPilot.Forcing.SetFormula.exConditions line 195
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_allConditions line 206
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_exConditions line 220