edit math

zmx0142857 · Oct 12, 2024 · bcccaaf · bcccaaf
1 parent 0c06304
commit bcccaaf
Show file tree

Hide file tree

Showing 5 changed files with 62 additions and 3 deletions.
diff --git a/js/toc.js b/js/toc.js
@@ -94,6 +94,7 @@ var tocData = [
           { "value": "3", "label": "二元关系与映射", "date": "2024-09-10" },
           { "value": "4", "label": "自然数与序数", "date": "2024-10-08" },
           { "value": "5", "label": "基数", "date": "2024-09-28" },
+          { "value": "6", "label": "类型论", "date": "2024-10-08" },
           { "value": "7", "label": "Lambda 表达式", "date": "2023-01-07" },
           { "value": "8", "label": "范畴论基础", "date": "2024-09-25" }
         ]

diff --git a/math/img/young-inequality.svg b/math/img/young-inequality.svg
diff --git a/math/misc/3.html b/math/misc/3.html
@@ -290,16 +290,18 @@ <h3>Jensen - Young - Hölder - Minkowski</h3>
 	</span>
 </p>
 
-<p class="remark">
+<div class="remark p">
 	Young 不等式的几何解释: 令 `y = x^(p-1)`, 则 `x = y^(q-1)`,
 	即 `y = x^(p-1)` 和 `x = y^(q-1)` 表示同一条曲线. 由积分的几何意义,
 	矩形的面积小于等于两个曲边三角形的面积之和, 即
 	<span class="formula">
 		`a b le int_0^a x^(p-1) dx + int_0^b y^(q-1) dy`
 		`= a^p/p + b^q/q`.
 	</span>
-	<img src="" alt="[图片暂缺]">
-</p>
+    <div class="img md" title="young 不等式">
+      <img src="../img/young-inequality.svg" alt="">
+    </div>
+</div>
 
 <p class="theorem">
 	<b>Hölder 不等式 (Hardy 不等式)</b>

diff --git a/math/set/1.html b/math/set/1.html
@@ -0,0 +1,12 @@
+<!DOCTYPE html>
+<html lang="zh-cn">
+<head>
+    <title>数理逻辑</title>
+    <meta charset="utf-8" />
+    <link rel="stylesheet" type="text/css" href="../../css/note.css" />
+</head>
+<body>
+
+<script src="../../js/note.js?type=math"></script>
+</body>
+</html>
diff --git a/math/set/6.html b/math/set/6.html
@@ -0,0 +1,43 @@
+<!DOCTYPE html>
+<html lang="zh-cn">
+<head>
+    <title>类型论</title>
+    <meta charset="utf-8" />
+    <link rel="stylesheet" type="text/css" href="../../css/note.css" />
+</head>
+<body>
+
+[来自《Homotopy Type Theory》, 又名 HoTT Book]
+
+<p class="remark">
+  和 ZFC 集合论类似, 类型论 (type theory) 也是数学的一门基础语言.
+</p>
+
+<ol class="definition">
+  <li><b>类型 (type)</b> 是类型论的基本概念. 用大写字母 `A, B, C...` 表示.</li>
+  <li><b>记号 `a: A`</b> 读作 "`a` 具有类型 `A`".
+    在类型论中, 每个变量都唯一地具有某种类型, 因此不能孤立地谈论一个变量 `a`.
+    类比于某些编程语言, 变量在声明时就已经决定了其类型, 我们不能引入一个变量却不声明其类型.
+    在一阶逻辑中, `a: A` 可以解释为 "命题 `A` 有一个证明", 或者说 `a` 是 `A` 有一个证明的 "证据".
+    因此在类型论中, 证明一个命题相当于构造一个变量 `a: A`.
+    <br>
+    在集合论中, `a: A` 又可以解释为 `a` 是集合 `A` 的元素.
+    一个重要的区别是, `a in A` 是一个命题而 `a: A` 不是.
+    在类型论的框架内, `a: A` 既已写出, 就是成立的. 我们不能证伪 `a: A`, 亦不能说
+    "如果 `a: A` 那么 `b: B` 不成立" 等.
+  </li>
+  <li><b>定义相等</b>
+    如果 `a, b: A` (即 `a: A`, `b: A`) 且它们根据定义是相等的, 就记作 `a := b: A` 或简写为 `a := b`.
+    例如对于函数 `f(x) = x^2`, 根据定义有 `f(3) := 3^2`.
+    同样地 `a := b` 不是一个命题, 否定它是没有意义的.
+  </li>
+  <li><b>命题相等</b> 由于类型论中的命题都是类型, 所以命题 `a = b` 也是一个类型, 记作 `a =_A b`.
+    这里 `a, b: A`.
+  </li>
+  <li><b>函数</b> 用记号 `f: A to B` 表示 `f` 是 `A` 到 `B` 的函数, 这里 `A to B` 也是一个类型.
+  </li>
+</ol>
+
+<script src="../../js/note.js?type=math"></script>
+</body>
+</html>