OAI/SetTheory/PartitionPrinciple/Forcing/GenericPartialFunctions.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Dense line 13
  2. def OAI.PartitionPilot.Forcing.DownwardClosed line 15
  3. def OAI.PartitionPilot.Forcing.CountablyClosed line 17
  4. structure OAI.PartitionPilot.Forcing.ConditionFilter line 20
  5. def OAI.PartitionPilot.Forcing.ConditionFilter.Meets line 28
  6. def OAI.PartitionPilot.Forcing.ConditionFilter.GenericFor line 30
  7. theorem OAI.PartitionPilot.Forcing.ConditionFilter.top_mem line 33
  8. theorem OAI.PartitionPilot.Forcing.ConditionFilter.compatible line 37
  9. structure OAI.PartitionPilot.Forcing.CountableCondition line 52
  10. theorem OAI.PartitionPilot.Forcing.CountableCondition.ext line 59
  11. instance OAI.PartitionPilot.Forcing.CountableCondition.(instance at line 65) line 65
  12. def OAI.PartitionPilot.Forcing.CountableCondition.domain line 82
  13. def OAI.PartitionPilot.Forcing.CountableCondition.empty line 84
  14. instance OAI.PartitionPilot.Forcing.CountableCondition.(instance at line 88) line 88
  15. theorem OAI.PartitionPilot.Forcing.CountableCondition.value_eq_of_le line 92
  16. theorem OAI.PartitionPilot.Forcing.CountableCondition.domain_mono line 98
  17. def OAI.PartitionPilot.Forcing.CountableCondition.assign line 104
  18. theorem OAI.PartitionPilot.Forcing.CountableCondition.assign_same line 113
  19. theorem OAI.PartitionPilot.Forcing.CountableCondition.assign_other line 118
  20. theorem OAI.PartitionPilot.Forcing.CountableCondition.assign_le line 123
  21. def OAI.PartitionPilot.Forcing.CountableCondition.definedAt line 133
  22. theorem OAI.PartitionPilot.Forcing.CountableCondition.definedAt_downwardClosed line 135
  23. theorem OAI.PartitionPilot.Forcing.CountableCondition.definedAt_dense line 139
  24. theorem OAI.PartitionPilot.Forcing.CountableCondition.compatible_values line 151
  25. theorem OAI.PartitionPilot.Forcing.exists_filter_meeting_sequence line 166
  26. theorem OAI.PartitionPilot.Forcing.exists_generic_for_countable_family line 188
  27. def OAI.PartitionPilot.Forcing.Compatible line 213
  28. def OAI.PartitionPilot.Forcing.DenseBelow line 215
  29. def OAI.PartitionPilot.Forcing.Localized line 217
  30. theorem OAI.PartitionPilot.Forcing.localized_dense line 219
  31. theorem OAI.PartitionPilot.Forcing.ConditionFilter.meets_below line 228
  32. theorem OAI.PartitionPilot.Forcing.denseBelow_mono line 235
  33. theorem OAI.PartitionPilot.Forcing.dense_countable_intersection line 246
  34. theorem OAI.PartitionPilot.Forcing.dense_simultaneous_witnesses line 261
  35. def OAI.PartitionPilot.Forcing.CountableCondition.Agrees line 280
  36. theorem OAI.PartitionPilot.Forcing.CountableCondition.agrees_symm line 283
  37. def OAI.PartitionPilot.Forcing.CountableCondition.merge line 286
  38. theorem OAI.PartitionPilot.Forcing.CountableCondition.merge_le_left line 300
  39. theorem OAI.PartitionPilot.Forcing.CountableCondition.merge_le_right line 305
  40. theorem OAI.PartitionPilot.Forcing.CountableCondition.merge_value line 312
  41. theorem OAI.PartitionPilot.Forcing.CountableCondition.merge_agrees line 323
  42. theorem OAI.PartitionPilot.Forcing.CountableCondition.three_agree_common line 330
  43. def OAI.PartitionPilot.Forcing.CountableCondition.unionValue line 342
  44. theorem OAI.PartitionPilot.Forcing.CountableCondition.unionValue_domain line 346
  45. theorem OAI.PartitionPilot.Forcing.CountableCondition.unionValue_extends line 359
  46. def OAI.PartitionPilot.Forcing.CountableCondition.chainUnion line 370
  47. theorem OAI.PartitionPilot.Forcing.CountableCondition.chainUnion_le line 375
  48. theorem OAI.PartitionPilot.Forcing.CountableCondition.countablyClosed line 379
  49. structure OAI.PartitionPilot.Forcing.DecisionSystem line 390
  50. def OAI.PartitionPilot.Forcing.DecisionSystem.commonDecisions line 399
  51. theorem OAI.PartitionPilot.Forcing.DecisionSystem.commonDecisions_dense line 401
  52. theorem OAI.PartitionPilot.Forcing.DecisionSystem.commonDecisions_downwardClosed line 404
  53. def OAI.PartitionPilot.Forcing.DecisionSystem.Realizes line 408
  54. theorem OAI.PartitionPilot.Forcing.DecisionSystem.compatible_decisions line 411
  55. theorem OAI.PartitionPilot.Forcing.DecisionSystem.realizes_unique line 416
  56. theorem OAI.PartitionPilot.Forcing.DecisionSystem.common_condition_decides line 423
  57. theorem OAI.PartitionPilot.Forcing.DecisionSystem.generic_condition_decides line 430
  58. theorem OAI.PartitionPilot.Forcing.CountableCondition.exists_value line 446
  59. def OAI.PartitionPilot.Forcing.CountableCondition.readValue line 453
  60. theorem OAI.PartitionPilot.Forcing.CountableCondition.readValue_realized line 456
  61. theorem OAI.PartitionPilot.Forcing.CountableCondition.readValue_of_condition line 460
  62. theorem OAI.PartitionPilot.Forcing.CountableCondition.readValue_iff line 466
  63. def OAI.PartitionPilot.Forcing.CountableCondition.coordinateDecisions line 475
  64. theorem OAI.PartitionPilot.Forcing.CountableCondition.coordinate_commonDecisions_dense line 490
  65. theorem OAI.PartitionPilot.Forcing.CountableCondition.readValue_sequence_decided line 494