OAI/Analysis/Naimark/Omission.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.PeakingPairData.AmbientPresentation line 15
  2. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.generated line 20
  3. theorem OAI.NaimarkZFC.PeakingPairData.ambient_presentation_swap line 40
  4. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.inherited line 69
  5. theorem OAI.NaimarkZFC.PeakingPairData.ambient_presentation_inherited line 104
  6. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.congr line 121
  7. theorem OAI.NaimarkZFC.HNNWord.AllCoefficients.mono line 139
  8. theorem OAI.NaimarkZFC.HNNWord.allCoefficients_one_stage line 145
  9. theorem OAI.NaimarkZFC.HNNWord.lift_reduced line 161
  10. lemma OAI.NaimarkZFC.PeakingPairData.turnCenter_natural line 188
  11. lemma OAI.NaimarkZFC.PeakingPairData.turnRemainder_natural line 195
  12. lemma OAI.NaimarkZFC.PeakingPairData.turnCentered_natural_iff line 202
  13. def OAI.NaimarkZFC.PeakingPairData.turnRemainderCLM line 210
  14. lemma OAI.NaimarkZFC.PeakingPairData.turnRemainderCLM_apply line 213
  15. lemma OAI.NaimarkZFC.PeakingPairData.inherited_turn line 229
  16. lemma OAI.NaimarkZFC.PeakingPairData.union_turnCenter_stable line 238
  17. lemma OAI.NaimarkZFC.PeakingPairData.limit_reduced_moment line 246
  18. theorem OAI.NaimarkZFC.PeakingPairData.hnn_directed_limit_presentation line 265
  19. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.directed_limit line 306
  20. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.le line 365
  21. theorem OAI.NaimarkZFC.PeakingPairData.ambient_presentation_directed_limit line 380
  22. def OAI.NaimarkZFC.omittedIndices line 417
  23. lemma OAI.NaimarkZFC.omittedIndices_mono line 420
  24. lemma OAI.NaimarkZFC.omittedIndices_zero line 427
  25. lemma OAI.NaimarkZFC.omittedIndices_succ line 432
  26. lemma OAI.NaimarkZFC.omittedIndices_succ_of_not_mem line 446
  27. lemma OAI.NaimarkZFC.omittedIndices_succ_of_lt line 456
  28. lemma OAI.NaimarkZFC.omittedIndices_subset_Iio line 464
  29. lemma OAI.NaimarkZFC.omittedIndices_insert_eq line 470
  30. lemma OAI.NaimarkZFC.omittedIndices_iUnion line 484
  31. def OAI.NaimarkZFC.omittedAlgebra line 498
  32. instance OAI.NaimarkZFC.omittedAlgebra_isClosed line 502
  33. instance OAI.NaimarkZFC.omittedAlgebra_cstar line 506
  34. lemma OAI.NaimarkZFC.omittedAlgebra_mono line 510
  35. lemma OAI.NaimarkZFC.omittedAlgebra_hnnGenerated line 514
  36. lemma OAI.NaimarkZFC.omittedAlgebra_continuous line 522
  37. lemma OAI.NaimarkZFC.directed_starSubalgebra_ranges line 536
  38. lemma OAI.NaimarkZFC.hnnGenerated_eq_of_mem line 555
  39. lemma OAI.NaimarkZFC.omittedAlgebra_zero line 567
  40. lemma OAI.NaimarkZFC.omittedAlgebra_base_mono line 572
  41. lemma OAI.NaimarkZFC.omittedAlgebra_le_chronological line 579
  42. lemma OAI.NaimarkZFC.omittedAlgebra_contains_initial line 584
  43. lemma OAI.NaimarkZFC.omittedAlgebra_succ_of_not_mem line 589
  44. lemma OAI.NaimarkZFC.omittedAlgebra_succ_of_lt line 594
  45. lemma OAI.NaimarkZFC.omittedAlgebra_succ line 599
  46. lemma OAI.NaimarkZFC.omittedAlgebra_succ_of_one line 607
  47. lemma OAI.NaimarkZFC.dense_subalgebra_inclusion_ranges line 622
  48. lemma OAI.NaimarkZFC.PeakingPairData.subalgebra_inclusion_ranges_directed line 659
  49. theorem OAI.NaimarkZFC.PeakingPairData.ambient_presentation_ordinal_limit line 671
  50. def OAI.NaimarkZFC.PeakingPairData.OmittedModel line 711
  51. lemma OAI.NaimarkZFC.PeakingPairData.omitted_model_successor line 717
  52. lemma OAI.NaimarkZFC.PeakingPairData.omitted_model_limit line 758
  53. lemma OAI.NaimarkZFC.PeakingPairData.omitted_model_zero line 773
  54. lemma OAI.NaimarkZFC.PeakingPairData.ordinal_invariant line 779
  55. theorem OAI.NaimarkZFC.PeakingPairData.omitted_presentation_of_chronological line 792
  56. lemma OAI.NaimarkZFC.PeakingPairData.states_eq_of_ambient_peaks line 811
  57. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.bridge line 818
  58. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.no_unintended_join line 832
  59. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_class_exclusions line 873
  60. theorem OAI.NaimarkZFC.PeakingPairData.ambient_preserves_omitted_inequivalence line 912
  61. lemma OAI.NaimarkZFC.PeakingPairData.ambient_identity_bridge line 946
  62. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.bridge line 952
  63. lemma OAI.NaimarkZFC.PeakingPairData.omitted_active_bridge line 972
  64. theorem OAI.NaimarkZFC.PeakingPairData.omitted_successor_bridge line 995
  65. lemma OAI.NaimarkZFC.PeakingPairData.subalgebra_simple_congr line 1038
  66. theorem OAI.NaimarkZFC.PeakingPairData.ambient_bridge_ordinal_simple line 1043
  67. theorem OAI.NaimarkZFC.PeakingPairData.ambient_bridge_ordinal_pureUEP line 1056
  68. lemma OAI.NaimarkZFC.PeakingPairData.joined_of_conjugacy line 1080
  69. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.joined line 1088
  70. lemma OAI.NaimarkZFC.PeakingPairData.AmbientPresentation.joined line 1107
  71. lemma OAI.NaimarkZFC.PeakingPairData.joined_onSubalgebra_larger line 1117
  72. def OAI.NaimarkZFC.PeakingPairData.PairDistinctOn line 1137
  73. lemma OAI.NaimarkZFC.PeakingPairData.PairDistinctOn.congr line 1143
  74. theorem OAI.NaimarkZFC.PeakingPairData.inherited_successor_bridge line 1161
  75. theorem OAI.NaimarkZFC.PeakingPairData.inherited_simple line 1188
  76. lemma OAI.NaimarkZFC.PeakingPairData.dependency_peaks_omitted line 1209
  77. lemma OAI.NaimarkZFC.omittedAlgebra_all_before line 1227
  78. lemma OAI.NaimarkZFC.omittedAlgebra_endpoint_eq_retained line 1235
  79. lemma OAI.NaimarkZFC.retainedOrdinal_succ_generated line 1248
  80. lemma OAI.NaimarkZFC.retainedOrdinal_succ_of_one line 1268
  81. lemma OAI.NaimarkZFC.retainedOrdinal_endpoint line 1274
  82. lemma OAI.NaimarkZFC.PeakingPairData.ambient_bridge_congr line 1285
  83. theorem OAI.NaimarkZFC.PeakingPairData.chronological_simple line 1295
  84. theorem OAI.NaimarkZFC.PeakingPairData.omitted_simple_of_chronological line 1325
  85. lemma OAI.NaimarkZFC.generatedFamily_Iio_mono line 1352
  86. lemma OAI.NaimarkZFC.PeakingPairData.chronological_joined line 1361
  87. theorem OAI.NaimarkZFC.PeakingPairData.ambient_pair_ordinal_inequivalent line 1392
  88. lemma OAI.NaimarkZFC.PeakingPairData.omitted_active_preserves_distinct line 1417
  89. lemma OAI.NaimarkZFC.PeakingPairData.omitted_distinct_successor line 1462
  90. theorem OAI.NaimarkZFC.PeakingPairData.omitted_distinct_of_chronological line 1513
  91. theorem OAI.NaimarkZFC.PeakingPairData.omitted_endpoint_bridge line 1528
  92. theorem OAI.NaimarkZFC.PeakingPairData.dependency_closed_retained_simple line 1565
  93. theorem OAI.NaimarkZFC.PeakingPairData.dependency_closed_retained_successor line 1575
  94. theorem OAI.NaimarkZFC.PeakingPairData.dependency_closed_pureUEP line 1596
  95. lemma OAI.NaimarkZFC.generatedFamily_reindex line 1613
  96. lemma OAI.NaimarkZFC.generatedFamily_map line 1620
  97. lemma OAI.NaimarkZFC.subalgebra_pureUEP_congr line 1631
  98. lemma OAI.NaimarkZFC.subalgebra_pureRestriction_congr line 1641
  99. lemma OAI.NaimarkZFC.subalgebraSubtype_pureUEP_of_top line 1648
  100. lemma OAI.NaimarkZFC.PeakingPairData.literal_dependency_closed_pureUEP line 1677
  101. lemma OAI.NaimarkZFC.PeakingPairData.literal_dependency_closed_ambientUEP line 1689
  102. theorem OAI.NaimarkZFC.PeakingPairData.literal_countable_determination line 1699
  103. theorem OAI.NaimarkZFC.countableSubsets_le_continuum line 1756
  104. theorem OAI.NaimarkZFC.cardinal_of_countable_determination line 1763
  105. theorem OAI.NaimarkZFC.continuous_eq_of_dense_values line 1789
  106. theorem OAI.NaimarkZFC.continuousMaps_le_continuum line 1795
  107. theorem OAI.NaimarkZFC.generatedFamily_pureStates_le_continuum line 1817
  108. lemma OAI.NaimarkZFC.subalgebra_uniqueRestriction_congr line 1853
  109. theorem OAI.NaimarkZFC.PeakingPairData.literal_pureStates_le_continuum line 1881
  110. theorem OAI.NaimarkZFC.exists_pureState_list line 1909