OAI/SetTheory/PartitionPrinciple/Forcing/GroundNameSequenceForcingWitness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.sequenceDecision line 14
  2. theorem OAI.PartitionPilot.Forcing.Name.sequenceDecision_mono line 18
  3. def OAI.PartitionPilot.Forcing.SetFormula.nameSequenceDecisionFormula line 26
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_nameSequenceDecisionFormula line 37
  5. def OAI.PartitionPilot.Forcing.Name.sequenceDecisionRelation line 93
  6. theorem OAI.PartitionPilot.Forcing.Name.mem_sequenceDecisionRelation line 98
  7. theorem OAI.PartitionPilot.Forcing.Name.sequenceDecisionRelation_entry line 108
  8. def OAI.PartitionPilot.Forcing.SetFormula.nameSequenceDecisionEntryFormula line 127
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_nameSequenceDecisionEntryFormula line 138
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sequenceDecisionRelation_mem line 185
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.sequenceFunctionNameEnv line 229
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sequenceFunction_eval line 237
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sequenceDecision_reading line 255
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sequenceDecision_unique_below line 266
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.sequenceDecision_dense_below line 286
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_sequenceFunction_forcing line 314