OAI/SetTheory/PartitionPrinciple/Definability/CountableSetFormulas.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.SetFormula.map_extend line 15
  2. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_ex line 23
  3. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_disj line 29
  4. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_imp line 35
  5. abbrev OAI.PartitionPilot.Forcing.SetFormula.Assignment line 51
  6. def OAI.PartitionPilot.Forcing.SetFormula.Forces line 53
  7. theorem OAI.PartitionPilot.Forcing.SetFormula.forces_mono line 60
  8. theorem OAI.PartitionPilot.Forcing.SetFormula.forces_of_dense line 70
  9. theorem OAI.PartitionPilot.Forcing.SetFormula.not_forces_refine_neg line 86
  10. theorem OAI.PartitionPilot.Forcing.SetFormula.forces_ex_iff line 95
  11. def OAI.PartitionPilot.Forcing.SetFormula.evalAssignment line 110
  12. theorem OAI.PartitionPilot.Forcing.SetFormula.evalAssignment_extend line 114
  13. def OAI.PartitionPilot.Forcing.SetFormula.liftIndex line 127
  14. theorem OAI.PartitionPilot.Forcing.SetFormula.extend_liftIndex line 130
  15. def OAI.PartitionPilot.Forcing.SetFormula.reindex line 136
  16. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_reindex line 143
  17. def OAI.PartitionPilot.Forcing.SetFormula.DecisionWitness line 169
  18. theorem OAI.PartitionPilot.Forcing.SetFormula.decisionWitness_dense line 172
  19. def OAI.PartitionPilot.Forcing.SetFormula.AllDecisionWitness line 181
  20. theorem OAI.PartitionPilot.Forcing.SetFormula.allDecisionWitness_dense line 185
  21. def OAI.PartitionPilot.Forcing.SetFormula.formulaFamily line 197
  22. def OAI.PartitionPilot.Forcing.SetFormula.extendMany line 210
  23. def OAI.PartitionPilot.Forcing.SetFormula.prefixIndex line 215
  24. def OAI.PartitionPilot.Forcing.SetFormula.suffixIndex line 219
  25. theorem OAI.PartitionPilot.Forcing.SetFormula.extendMany_prefix line 223
  26. theorem OAI.PartitionPilot.Forcing.SetFormula.extendMany_suffix line 231
  27. theorem OAI.PartitionPilot.Forcing.SetFormula.extendMany_members line 238
  28. def OAI.PartitionPilot.Forcing.SetFormula.exBlock line 249
  29. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_exBlock line 253
  30. def OAI.PartitionPilot.Forcing.SetFormula.conjBlock line 279
  31. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_conjBlock line 283
  32. theorem OAI.PartitionPilot.Forcing.SetFormula.forcing_truth line 304
  33. theorem OAI.PartitionPilot.Forcing.SetFormula.forces_sound line 351
  34. theorem OAI.PartitionPilot.Forcing.SetFormula.ex_witness_in_filter line 357
  35. def OAI.PartitionPilot.Forcing.SetFormula.allBlock line 376
  36. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_allBlock line 380
  37. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_extensionality line 406
  38. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_foundation line 416
  39. theorem OAI.PartitionPilot.Forcing.SetFormula.basic_axioms_in_generic line 434
  40. def OAI.PartitionPilot.Forcing.SetFormula.natCode line 452
  41. theorem OAI.PartitionPilot.Forcing.SetFormula.natCode_injective line 459
  42. instance OAI.PartitionPilot.Forcing.SetFormula.countable line 500