Merge pull request #41 from ChiyoYuki/master

fix: fix some bugs.

Author: subfish-zhou

.github/workflows/deploy.yml

@@ -36,7 +36,6 @@ jobs:
 
       - name: Run build script
         run: |
-          chmod +x scripts/mkall.py
           python scripts/mkall.py
           make html
           touch ./build/html/.nojekyll

1.lean

@@ -114,7 +114,7 @@ def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
 /- TEXT:
 .. index:: lambda abstraction
 
-在下一个例子中， ``fun x ↦ f x + g x`` 是把 ``x`` 映射到 `` f x + g x`` 的函数。从表达式 ``f x + g x`` 构造这个函数的过程在类型论中称为 lambda 抽象 （lambda abstraction）。
+在下一个例子中， ``fun x ↦ f x + g x`` 是把 ``x`` 映射到 ``f x + g x`` 的函数。从表达式 ``f x + g x`` 构造这个函数的过程在类型论中称为 lambda 抽象 （lambda abstraction）。
 BOTH: -/
 section
 variable (f g : ℝ → ℝ) (a b : ℝ)

MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean

@@ -162,6 +162,7 @@ noncomputable example (f : V →ₗ[K] W) (h : Function.Bijective f) : V ≃ₗ[
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 我们可以利用已有的向量空间，通过直和和直积构造新的向量空间。从两个向量空间开始，在该情形下直和与直积无区别，我们可以直接使用积类型。在以下代码片段中，我们展示了如何将所有结构映射（包含关系与投影）表示为线性映射，同时演示了通过泛性质构造积的输入线性映射与和的输出线性映射的方法（若您不熟悉范畴论中积与和的区分，可忽略泛性质相关术语，重点关注后续示例的类型特征）。
+EXAMPLES: -/
 -- QUOTE:
 
 section binary_product