1. notice
  3. English
  5. logic-topic
  6. 1. logic
  7. 2. set-theory
  8. 3. map
  9. 4. order
  10. 5. combinatorics
  12. calculus
  13. 6. real-numbers
  14. 7. limit-sequence
  15. 8. ℝ^n
  16. 9. Euclidean-space
  17. 10. Minkowski-space
  18. 11. polynomial
  19. 12. analytic-Euclidean
  20. 13. analytic-Minkowski
  21. 14. analytic-struct-operation
  22. 15. ordinary-differential-equation
  23. 16. volume
  24. 17. integral
  25. 18. divergence
  26. 19. limit-net
  27. 20. topology
  28. 21. compact
  29. 22. connected
  30. 23. topology-struct-operation
  31. 24. exponential
  32. 25. angle
  34. geometry
  35. 26. manifold
  36. 27. metric
  37. 28. metric-connection
  38. 29. geodesic-derivative
  39. 30. curvature-of-metric
  40. 31. Einstein-metric
  41. 32. constant-sectional-curvature
  42. 33. simple-symmetric-space
  43. 34. principal-bundle
  44. 35. group-action
  45. 36. stereographic-projection
  46. 37. Hopf-bundle
  48. field-theory
  49. 38. point-particle-non-relativity
  50. 39. point-particle-relativity
  51. 40. scalar-field
  52. 41. scalar-field-current
  53. 42. scalar-field-non-relativity
  54. 43. projective-lightcone
  55. 44. spacetime-momentum-spinor-representation
  56. 45. Lorentz-group
  57. 46. spinor-field
  58. 47. spinor-field-current
  59. 48. electromagnetic-field
  60. 49. Laplacian-of-tensor-field
  61. 50. Einstein-metric
  62. 51. interaction
  63. 52. harmonic-oscillator-quantization
  64. 53. spinor-field-misc
  65. 54. reference
  67. 中文
  68. 55. notice
  70. 逻辑
  71. 56. 逻辑
  72. 57. 集合论
  73. 58. 映射
  74. 59. 序
  75. 60. 组合
  77. 微积分
  78. 61. 实数
  79. 62. 数列极限
  80. 63. ℝ^n
  81. 64. Euclidean 空间
  82. 65. Minkowski 空间
  83. 66. 多项式
  84. 67. 解析 (Euclidean)
  85. 68. 解析 (Minkowski)
  86. 69. 解析 struct 的操作
  87. 70. 常微分方程
  88. 71. 体积
  89. 72. 积分
  90. 73. 散度
  91. 74. 网极限
  92. 75. 拓扑
  93. 76. 紧致
  94. 77. 连通
  95. 78. 拓扑 struct 的操作
  96. 79. 指数函数
  97. 80. 角度
  99. 几何
  100. 81. 流形
  101. 82. 度规
  102. 83. 度规的联络
  103. 84. Levi-Civita 导数
  104. 85. 度规的曲率
  105. 86. Einstein 度规
  106. 87. 常截面曲率
  107. 88. simple-symmetric-space
  108. 89. 主丛
  109. 90. 群作用
  110. 91. 球极投影
  111. 92. Hopf 丛
  113. 场论
  114. 93. 非相对论点粒子
  115. 94. 相对论点粒子
  116. 95. 纯量场
  117. 96. 纯量场的守恒流
  118. 97. 非相对论纯量场
  119. 98. 光锥射影
  120. 99. 时空动量的自旋表示
  121. 100. Lorentz 群
  122. 101. 旋量场
  123. 102. 旋量场的守恒流
  124. 103. 电磁场
  125. 104. 张量场的 Laplacian
  126. 105. Einstein 度规
  127. 106. 相互作用
  128. 107. 谐振子量子化
  129. 108. 旋量场杂项
  130. 109. 参考

note-math

二元关系 := 命题函数 or 的子集

时称为 独立无关

元关系类似

[order]

命题函数 是序 :=

  • 传递:
  • 无环:

也可以用 "等价" 的 版本

  • 传递:
  • 自反
  • 反对称

等价是指

  • 如果先有 版本的偏序, 那么定义 之后就有 版本的偏序, 且能变回来 (变回来不是显然的, 需要 偏序的性质来证明, 下同)
  • 如果先有 版本的偏序, 那么定义 之后就有 版本的偏序, 且能变回来

Prop 偏序 ==> 非自反 Proof 如果 , 那么无环被破坏

注意: "非自反" (nonreflexive) 不是 not 自反 (not reflexive)

Prop 偏序 ==> ( ) Proof 如果 那么就有

Def

Prop 假设 偏序, 则

Proof

但是偏序 ==> , 所以

Prop 假设 偏序, 则 Proof

但是偏序 ==>

Proof <== 显然. 对于 ==>, 假设 . 如果 则由于 , 有 . 如果 那么

Prop (证明不需要 的偏序性质)

  • 是自反的
  • 是非自反的

Prop 的无环性质 ==> 的反对称性质

Prop 的反对称性质 ==> 的无环性质

Prop 传递 ==> 传递

Prop 传递 + 反对称 ==> 传递

这些命题加起来就证明了 偏序的等价性

Example

  • 子集的 "包含" , 或者 "包含且不等于" , 是序

    image modified from wiki media about partial order

  • 的
  • 树图

[order-comparable] comparable :=

[comparable-component] is comparable-component :=

偏序可以分解为相互不 comparable 的 comparable-component. 想象两个毫无关系的树图

[linear-order] 线序

直观上, 线序没有分支, 也称为 "链"

[maximal-linear-order] 极大线序链

let with 线序. is maximal-linear-order := 以下定义等价

它并不能用于分解偏序. 两个极大线序链可以有相交的部分

等价地

  • 链无法延拓

链的延拓是指, 存在 且 , 使得, 对每个 , . 延拓后, 也是链

[maximal-linear-order-exists] maximal-linear-order chain alaways exists

也称为 Zorn 引理

需要 选择公理: 如果能够对 (某个类型的) 一些集合证明按照存在某种性质的元素, 那么可以定义一个函数, 将这些集合映射到对应的元素

Proof (ref-29) (ported from formal proof in zorn_lemma.ac in my github repo ac-math ref-30)

可以用 的所有区间的 偏序, 作为直观例子. 区间链 就是, 对每个区间 都有 或

假设没有极大链, 那么每个链都是可延拓的

根据选择公理, 可以构造延拓函数 的定义域是 , 值域是 , 是延拓元

Def 链 的 " " 或者 "后继"

Def 链 之间的可比较定义为 或

Def 可比较的链集, 或者线性链集 .

Prop 线性链集 对自己的元素进行并集 得到的是 的链

Proof

对每个 , 存在 使得 .

如果 那么 是 可比较的

如果 那么 是 可比较的

Def 归纳链集 且满足,

  • 包含零元或者归纳初始元.
  • 包含 "+1". 对每个 , 其后继也

  • 线性链集的并集也是归纳链. 如果 是线性链集 , 则

    似乎类似于 的 "强归纳法": (对 , 正确 ==> 正确) ==> 对所有 , 正确

Prop 归纳链集存在. 所有 链的集合 就满足 所需要的所有性质

Def 最小归纳链集 :=

Prop 是归纳链集

Proof 证明归纳链集的性质对闭集封闭

  • 零元.
属于每个 , 从而也属于
  • +1

对每个链

对每个

从而

  • 强归纳

设 是线性链

对每个

从而

Def 最小归纳链集里的可比较链 且满足

  • 对每个 都链可比较

Prop 是归纳链集

  • 从而
  • 从而

Proof

  • 零元
空链 因为 其它链, 从而是可比较链,
  • . 如果 是可比较链, 那么 也是可比较链

Prop 对 , 如果 , 则

Proof 是可比较链, 所以 可比较. . 用反证法, 假设 得到矛盾

因为 就是我们要证明的, 所以需要绕过它

Def 设 是可比较链, 定义为 且满足

  • or

Prop 是可归纳集

Proof

  • 零元
  • "+1"

设

  • 如果 , 如前所述
  • 如果 , 则 从而
  • 如果 , 则

从而 or

从而

  • 强归纳

设

对 , 取 使得

or

==>

从而

回来继续证明 的 性质, 证明

对于

  • 如果 则根据 的定义,

从而 or

从而

  • 强归纳

设 且

对于

  • 如果每个 都 那么
  • 如果有一个 使得 那么

从而 可比较, 从而

Prop 是线性链集

Proof 使用

  • 的性质, 以及

从而最小归纳链集 也是线性链集

Prop

Prop 是链

Prop 是极大链

Proof

定义

假设 不是最大链

由归纳链集的性质,

, 所以

也即

这与 矛盾, 根据链延拓函数 的定义