OAI/SetTheory/PartitionPrinciple/Definability/PreservedMainPrefixHistoryFormulas.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.nonzeroLimitOrdinalFormula line 12
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_nonzeroLimitOrdinalFormula line 15
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_nonzeroLimitOrdinalFormula line 21
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.mainPrefixFieldExtensionFormula line 33
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainPrefixFieldExtensionFormula line 36
  6. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixExtensionFormula line 45
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixExtensionFormula line 59
  8. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixLimitStepRawFormula line 97
  9. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixLimitStepFormula line 110
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixLimitStepRawFormula line 120
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixLimitStepFormula line 139
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.mainPrefixSelectedStepBody line 164
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainPrefixSelectedStepBody line 175
  14. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixSelectedStepFormula line 194
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixSelectedStepFormula line 204
  16. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixConditionalStepFormula line 247
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixConditionalStepFormula line 262
  18. def OAI.PartitionPilot.Forcing.SetFormula.preservedMainPrefixHistoryValuesFormula line 307
  19. def OAI.PartitionPilot.Forcing.SetFormula.preservedMainPrefixHistoryCompatibilityFormula line 314
  20. def OAI.PartitionPilot.Forcing.SetFormula.preservedMainPrefixHistoryFormula line 323
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preservedMainPrefixHistoryValuesFormula line 333
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preservedMainPrefixHistoryCompatibilityFormula line 375
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preservedMainPrefixHistoryFormula line 406