OAI/SetTheory/PartitionPrinciple/Forcing/InitialRowForcing.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.CountableCondition.rename line 14
  2. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_value line 20
  3. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_refl line 25
  4. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_trans line 27
  5. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_symm line 30
  6. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_le_iff line 35
  7. def OAI.PartitionPilot.Forcing.CountableCondition.renameOrderIso line 44
  8. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_top line 51
  9. theorem OAI.PartitionPilot.Forcing.CountableCondition.rename_fixed line 53
  10. def OAI.PartitionPilot.Forcing.CountableCondition.graphCode line 87
  11. theorem OAI.PartitionPilot.Forcing.CountableCondition.graphCode_injective line 90
  12. theorem OAI.PartitionPilot.Forcing.CountableCondition.cardinal_lt line 102
  13. abbrev OAI.PartitionPilot.Forcing.Rows.Conditions line 113
  14. def OAI.PartitionPilot.Forcing.Rows.differentRows line 115
  15. theorem OAI.PartitionPilot.Forcing.Rows.fresh_column line 118
  16. theorem OAI.PartitionPilot.Forcing.Rows.differentRows_dense line 128
  17. theorem OAI.PartitionPilot.Forcing.Rows.differentRows_downwardClosed line 144
  18. abbrev OAI.PartitionPilot.Forcing.Rows.Position line 150
  19. abbrev OAI.PartitionPilot.Forcing.Rows.RowForcing line 151
  20. theorem OAI.PartitionPilot.Forcing.Rows.rowForcing_countablyClosed line 153
  21. theorem OAI.PartitionPilot.Forcing.Rows.positions_cardinal_lt line 155
  22. theorem OAI.PartitionPilot.Forcing.Rows.coordinates_cardinal_lt line 158
  23. theorem OAI.PartitionPilot.Forcing.Rows.rowForcing_cardinal_lt line 163
  24. def OAI.PartitionPilot.Forcing.Rows.denseFamily line 180
  25. theorem OAI.PartitionPilot.Forcing.Rows.denseFamily_dense line 183
  26. theorem OAI.PartitionPilot.Forcing.Rows.generic_meets_coordinates line 188
  27. def OAI.PartitionPilot.Forcing.Rows.row line 192
  28. theorem OAI.PartitionPilot.Forcing.Rows.mem_row_iff line 196
  29. theorem OAI.PartitionPilot.Forcing.Rows.row_injective line 200
  30. theorem OAI.PartitionPilot.Forcing.Rows.actual_generic_rows line 214
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.act_inv_left line 228
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.act_inv_right line 231
  33. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.fixSubgroup line 234
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.fix_antitone line 242
  35. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.conjugateHom line 245
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.fix_conjugation line 250
  37. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.SupportedSubgroup line 267
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.supported_top line 269
  39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.supported_upward line 271
  40. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.supported_inf line 276
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.supported_conjugate line 285
  42. structure OAI.PartitionPilot.Compression.RecursiveMaps.NormalSubgroupFamily line 304
  43. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.supportFamily line 314
  44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.OrdinalRun.supportFamily_countably_complete line 326
  45. theorem OAI.PartitionPilot.Forcing.Rows.action_bottom line 347
  46. def OAI.PartitionPilot.Forcing.Rows.positionAction line 356
  47. theorem OAI.PartitionPilot.Forcing.Rows.positionAction_one line 363
  48. theorem OAI.PartitionPilot.Forcing.Rows.positionAction_mul line 366
  49. def OAI.PartitionPilot.Forcing.Rows.positionPermutation line 370
  50. def OAI.PartitionPilot.Forcing.Rows.coordinatePermutation line 376
  51. theorem OAI.PartitionPilot.Forcing.Rows.coordinatePermutation_one line 379
  52. theorem OAI.PartitionPilot.Forcing.Rows.coordinatePermutation_mul line 384
  53. def OAI.PartitionPilot.Forcing.Rows.rowAction line 390
  54. theorem OAI.PartitionPilot.Forcing.Rows.rowAction_one line 393
  55. theorem OAI.PartitionPilot.Forcing.Rows.rowAction_mul line 397
  56. theorem OAI.PartitionPilot.Forcing.Rows.rowAction_value line 403
  57. theorem OAI.PartitionPilot.Forcing.Rows.rowAction_top line 407
  58. theorem OAI.PartitionPilot.Forcing.Rows.rowAction_le_iff line 410
  59. theorem OAI.PartitionPilot.Forcing.Rows.rowCondition_supported line 414
  60. def OAI.PartitionPilot.Forcing.Rows.rowConditionPresentation line 439
  61. theorem OAI.PartitionPilot.Forcing.Rows.rowConditionPresentation_rank_lt line 441
  62. structure OAI.PartitionPilot.Forcing.Rows.InitialRowForcingLaws line 445
  63. theorem OAI.PartitionPilot.Forcing.Rows.initial_row_forcing_laws line 461