OAI/Analysis/Naimark/Homogeneity.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.KOS.Close line 17
  2. theorem OAI.NaimarkZFC.KOS.Close.symm line 21
  3. def OAI.NaimarkZFC.KOS.LocalControl line 27
  4. def OAI.NaimarkZFC.KOS.SameClassControl line 36
  5. theorem OAI.NaimarkZFC.KOS.inner_fitting line 45
  6. theorem OAI.NaimarkZFC.KOS.localControl_of_sameClassControl line 63
  7. structure OAI.NaimarkZFC.KOS.ControlData line 96
  8. theorem OAI.NaimarkZFC.KOS.exists_controlData line 107
  9. def OAI.NaimarkZFC.KOS.tests line 119
  10. theorem OAI.NaimarkZFC.KOS.mem_tests line 124
  11. def OAI.NaimarkZFC.KOS.orbitTests line 128
  12. theorem OAI.NaimarkZFC.KOS.step_control line 132
  13. theorem OAI.NaimarkZFC.KOS.restrict_trans line 149
  14. def OAI.NaimarkZFC.KOS.data line 155
  15. theorem OAI.NaimarkZFC.KOS.data_tests line 162
  16. theorem OAI.NaimarkZFC.KOS.data_radius line 169
  17. structure OAI.NaimarkZFC.KOS.Stage line 179
  18. def OAI.NaimarkZFC.KOS.Step line 185
  19. theorem OAI.NaimarkZFC.KOS.exists_next line 194
  20. theorem OAI.NaimarkZFC.KOS.exists_initial line 217
  21. theorem OAI.NaimarkZFC.KOS.exists_controlled_pair line 230
  22. theorem OAI.NaimarkZFC.KOS.cauchy_of_geometric_tests line 250
  23. theorem OAI.NaimarkZFC.KOS.homogeneity_of_localControl line 259
  24. theorem OAI.NaimarkZFC.KOS.homogeneity_of_sameClassControl line 293
  25. def OAI.NaimarkZFC.KOS.NearCentralRows line 307
  26. lemma OAI.NaimarkZFC.KOS.norm_inverse_inner_displacement line 316
  27. theorem OAI.NaimarkZFC.KOS.sameClassControl_of_nearCentralRows line 324
  28. theorem OAI.NaimarkZFC.KOS.homogeneity_of_nearCentralRows line 373
  29. lemma OAI.NaimarkZFC.KOS.rowAverage_norm line 387
  30. lemma OAI.NaimarkZFC.KOS.rowAverage_congruence line 400
  31. lemma OAI.NaimarkZFC.KOS.near_congruence_norm line 404
  32. lemma OAI.NaimarkZFC.KOS.commutator_congruence_norm line 429
  33. def OAI.NaimarkZFC.KOS.ApproxNearCentralRows line 450
  34. theorem OAI.NaimarkZFC.KOS.nearCentralRows_of_approx line 458
  35. theorem OAI.NaimarkZFC.KOS.homogeneity_of_approxRows line 488
  36. lemma OAI.NaimarkZFC.TracialStage.core_car_injective line 510
  37. lemma OAI.NaimarkZFC.TracialStage.core_infinite line 516
  38. lemma OAI.NaimarkZFC.TracialStage.core_reference_peaks line 523
  39. theorem OAI.NaimarkZFC.TracialStage.exists_supported_peak_pair line 528
  40. theorem OAI.NaimarkZFC.TracialStage.exists_joining_successor line 552
  41. def OAI.NaimarkZFC.starPair line 574
  42. lemma OAI.NaimarkZFC.starPair_false line 578
  43. lemma OAI.NaimarkZFC.starPair_true line 579
  44. lemma OAI.NaimarkZFC.star_starPair line 580
  45. lemma OAI.NaimarkZFC.map_hnnGenerated line 583
  46. lemma OAI.NaimarkZFC.hnnGenerated_self line 594
  47. lemma OAI.NaimarkZFC.generatedFamily_insert line 613
  48. lemma OAI.NaimarkZFC.hnnGenerated_eq_insert line 634
  49. lemma OAI.NaimarkZFC.StarAlgHom.equivClosedRange line 643
  50. lemma OAI.NaimarkZFC.StarAlgHom.range_comp_eq_map line 656
  51. theorem OAI.NaimarkZFC.PeakingPairData.inherited_ambient_presentation line 679
  52. def OAI.NaimarkZFC.PeakingPairData.onSubalgebra line 721
  53. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_peak line 725
  54. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_trace line 727
  55. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_state line 728
  56. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_unique line 731
  57. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_natural_peak line 738
  58. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_natural_trace line 742
  59. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_natural_state line 746
  60. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_unique_inclusion line 751
  61. lemma OAI.NaimarkZFC.PeakingPairData.onSubalgebra_inequivalent_of_larger line 759
  62. theorem OAI.NaimarkZFC.PeakingPairData.hnn_ambient_presentation line 780
  63. lemma OAI.NaimarkZFC.PeakingPairData.hnn_hom_ext line 827
  64. theorem OAI.NaimarkZFC.PeakingPairData.hnn_reorder_via_equivs line 841
  65. theorem OAI.NaimarkZFC.PeakingPairData.hnn_reorder_ambient_target line 890
  66. theorem OAI.NaimarkZFC.PeakingPairData.hnn_reorder_from_ambient_data line 960
  67. lemma OAI.NaimarkZFC.PeakingPairData.hnnGenerated_eq_top line 1007
  68. lemma OAI.NaimarkZFC.PeakingPairData.hnn_image_generated line 1013
  69. lemma OAI.NaimarkZFC.PeakingPairData.hnn_equiv_image_generated line 1025
  70. def OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation line 1050
  71. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.generated line 1061
  72. lemma OAI.NaimarkZFC.PeakingPairData.HNNAmbientPresentation.swap line 1072