OAI/Analysis/Naimark/Dependencies.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.generatedFamily line 13
  2. theorem OAI.NaimarkZFC.generatedFamily_mono line 16
  3. theorem OAI.NaimarkZFC.countable_submonoidClosure line 22
  4. theorem OAI.NaimarkZFC.separable_submonoidClosure line 28
  5. theorem OAI.NaimarkZFC.separable_starAdjoin line 36
  6. theorem OAI.NaimarkZFC.generatedFamily_separable line 45
  7. theorem OAI.NaimarkZFC.generatedFamily_isClosed line 50
  8. theorem OAI.NaimarkZFC.generatedFamily_contains_base line 53
  9. theorem OAI.NaimarkZFC.generatedFamily_contains line 57
  10. theorem OAI.NaimarkZFC.starAdjoin_countable_support line 61
  11. theorem OAI.NaimarkZFC.generatedFamily_countable_support line 90
  12. theorem OAI.NaimarkZFC.generatedFamily_iUnion line 100
  13. theorem OAI.NaimarkZFC.pure_state_excision_witness line 129
  14. def OAI.NaimarkZFC.DependencyClosed line 155
  15. def OAI.NaimarkZFC.dependencyStep line 157
  16. def OAI.NaimarkZFC.dependencyClosure line 159
  17. theorem OAI.NaimarkZFC.subset_dependencyStep line 162
  18. theorem OAI.NaimarkZFC.subset_dependencyClosure line 165
  19. theorem OAI.NaimarkZFC.dependencyClosure_closed line 169
  20. theorem OAI.NaimarkZFC.dependencyStep_countable line 178
  21. theorem OAI.NaimarkZFC.dependencyClosure_countable line 182
  22. theorem OAI.NaimarkZFC.exists_countable_dependencyClosure line 192
  23. theorem OAI.NaimarkZFC.DependencyClosed.iUnion line 198
  24. theorem OAI.NaimarkZFC.countable_witness_closure line 210
  25. theorem OAI.NaimarkZFC.pure_restrict_of_witnesses line 272
  26. theorem OAI.NaimarkZFC.countable_pure_restriction line 292
  27. theorem OAI.NaimarkZFC.generatedFamily_countable_pure_restriction line 324
  28. theorem OAI.NaimarkZFC.StateExtensionUnique.of_comp line 345
  29. theorem OAI.NaimarkZFC.PureUEP.of_comp line 358
  30. theorem OAI.NaimarkZFC.pure_restrict_of_unique_factor line 365
  31. theorem OAI.NaimarkZFC.pure_restrict_intermediate_subalgebra line 384
  32. theorem OAI.NaimarkZFC.countable_bounded_regular line 408
  33. abbrev OAI.NaimarkZFC.constructionCardinal line 425
  34. theorem OAI.NaimarkZFC.constructionCardinal_regular line 427
  35. theorem OAI.NaimarkZFC.countable_bounded_construction line 430
  36. theorem OAI.NaimarkZFC.construction_initial_cardinal_le line 436
  37. theorem OAI.NaimarkZFC.bounded_pure_determination line 451
  38. theorem OAI.NaimarkZFC.generatedFamily_eventual_pure_restriction line 465
  39. theorem OAI.NaimarkZFC.scheduled_pure_equivalent_to_reference line 489
  40. theorem OAI.NaimarkZFC.irreducible_nontrivial_space line 532
  41. theorem OAI.NaimarkZFC.car_no_finite_irreps line 541
  42. theorem OAI.NaimarkZFC.UnitarilyEquivalent.isIrreducible line 570
  43. theorem OAI.NaimarkZFC.irreducible_vector_pure_equivalent line 605
  44. theorem OAI.NaimarkZFC.all_irreducibles_equivalent_of_pure_states line 621
  45. def OAI.NaimarkZFC.HNNWord.AllCoefficients line 643
  46. theorem OAI.NaimarkZFC.HNNWord.reduced_approximation line 647
  47. theorem OAI.NaimarkZFC.hnn_reduced_vanish_of_dense line 681
  48. def OAI.NaimarkZFC.PeakingPairData.turnCenterCLM line 707
  49. theorem OAI.NaimarkZFC.PeakingPairData.turnCenterCLM_apply line 711
  50. theorem OAI.NaimarkZFC.PeakingPairData.turnCenter_fix line 714
  51. theorem OAI.NaimarkZFC.PeakingPairData.hnn_limit_comparison line 719
  52. theorem OAI.NaimarkZFC.isometry_cauchy_on_dense line 753
  53. def OAI.NaimarkZFC.autPointwiseLimit line 773
  54. theorem OAI.NaimarkZFC.tendsto_autPointwiseLimit line 776
  55. theorem OAI.NaimarkZFC.autPointwiseLimit_isometry line 780
  56. def OAI.NaimarkZFC.autLimitHom line 788
  57. theorem OAI.NaimarkZFC.autLimitHom_surjective line 806
  58. def OAI.NaimarkZFC.autLimitEquiv line 823
  59. theorem OAI.NaimarkZFC.autLimitEquiv_transports line 827
  60. theorem OAI.NaimarkZFC.cauchySeq_of_tail_geometric_steps line 839
  61. theorem OAI.NaimarkZFC.exists_automorphism_of_geometric_approximants line 850
  62. def OAI.NaimarkZFC.ordinalMajorant line 888
  63. theorem OAI.NaimarkZFC.le_ordinalMajorant line 893
  64. theorem OAI.NaimarkZFC.ordinalMajorant_strictMono line 898
  65. theorem OAI.NaimarkZFC.ordinalMajorant_lt line 907
  66. theorem OAI.NaimarkZFC.exists_injective_above line 920
  67. theorem OAI.NaimarkZFC.exists_pair_schedule line 950
  68. theorem OAI.NaimarkZFC.pure_state_finite_excision line 968
  69. theorem OAI.NaimarkZFC.compressed_vector_coefficient_bound line 999
  70. theorem OAI.NaimarkZFC.faithful_vector_pure_approximation line 1036
  71. theorem OAI.NaimarkZFC.simple_pure_inner_orbit_finite line 1065
  72. theorem OAI.NaimarkZFC.exists_inner_geometric_state_approximants line 1084
  73. theorem OAI.NaimarkZFC.generatedFamily_iUnion_directed line 1115
  74. theorem OAI.NaimarkZFC.generatedFamily_ordinal_continuous line 1146
  75. theorem OAI.NaimarkZFC.dense_iUnion_starSubalgebra_inclusions line 1180
  76. theorem OAI.NaimarkZFC.starSubalgebra_inclusion_comp line 1203
  77. def OAI.NaimarkZFC.retainedOrdinalAlgebra line 1208
  78. instance OAI.NaimarkZFC.retainedOrdinalAlgebra_isClosed line 1211
  79. instance OAI.NaimarkZFC.retainedOrdinalAlgebra_cstar line 1214
  80. def OAI.NaimarkZFC.retainedOrdinalInclusion line 1225
  81. theorem OAI.NaimarkZFC.retainedOrdinalInclusion_injective line 1231
  82. theorem OAI.NaimarkZFC.retainedOrdinalInclusion_continuous line 1236
  83. theorem OAI.NaimarkZFC.retainedOrdinalInclusion_refl line 1242
  84. theorem OAI.NaimarkZFC.retainedOrdinalInclusion_comp line 1249
  85. theorem OAI.NaimarkZFC.retainedOrdinal_pureUEP line 1256
  86. theorem OAI.NaimarkZFC.retainedOrdinalSucc_eq_of_mem line 1270
  87. theorem OAI.NaimarkZFC.retainedOrdinalSuccessor_identity line 1285
  88. theorem OAI.NaimarkZFC.retainedOrdinal_pureUEP_of_omitted line 1300
  89. theorem OAI.NaimarkZFC.PureStateEquivalent.symm line 1318
  90. theorem OAI.NaimarkZFC.PureStateEquivalent.trans line 1321
  91. theorem OAI.NaimarkZFC.PeakingPairData.hnnPush_class_exclusions line 1334
  92. theorem OAI.NaimarkZFC.PeakingPairData.hnnPush_swap_separated line 1377
  93. theorem OAI.NaimarkZFC.PeakingPairData.swap_map_of_equiv line 1395
  94. theorem OAI.NaimarkZFC.PeakingPairData.actual_omitted_swap line 1419