表現修正

Author: s-taiga

MIL/C08_Topology/S03_Topological_Spaces.lean

@@ -73,7 +73,7 @@ Closed sets are then defined as sets whose complement  is open. A function betwe
 is (globally) continuous if all preimages of open sets are open.
 OMIT. -/
 /- TEXT:
-また，閉集合はその補集合が開である集合として定義されます．位相空間の間の関数は開集合の逆像がずべて開であれば（大域的に）連続です．
+また，閉集合はその補集合が開である集合として定義されます．位相空間の間の関数は開集合の逆像がすべて開であれば（大域的に）連続です．
 BOTH: -/
 -- QUOTE:
 variable {Y : Type*} [TopologicalSpace Y]
@@ -123,7 +123,7 @@ equivalent to the previous one.
 
 OMIT. -/
 /- TEXT:
-また近傍を通常の集合，近傍フィルタを一般化された集合としてみなすことを両方もちいて，次のように記述することもできます．「 ``f x`` の任意の近傍 ``U`` に対して， ``x`` に近い点はすべて ``U`` に送られる」．この証明も ``iff.rfl`` で与えられ，この観点は前のものと定義上等価であることに注意してください．
+また近傍を通常の集合として，近傍フィルタを一般化された集合としてみなすことの両方を用いて，次のように記述することもできます．「 ``f x`` の任意の近傍 ``U`` に対して， ``x`` に近い点はすべて ``U`` に送られる」．この証明も ``iff.rfl`` で与えられ，この観点は前のものと定義上等価であることに注意してください．
 
 BOTH: -/
 -- QUOTE:
@@ -291,7 +291,7 @@ On paper we will use notations :math:`f_*T` for ``TopologicalSpace.coinduced f T
 :math:`f^*T` for ``TopologicalSpace.induced f T``.
 OMIT. -/
 /- TEXT:
-これらの操作は関数の合成でコンパクトにできます．例によって押し出しは共編であり，引き戻しは反変です（ ``coinduced_compose`` と ``induced_compose`` を参照）．本書では， ``TopologicalSpace.coinduced f T`` に対して :math:`f_*T` ， ``TopologicalSpace.induced f T`` に対して :math:`f^*T` という表記を使用します．
+これらの操作は関数の合成でコンパクトにできます．例によって押し出しは共変であり，引き戻しは反変です（ ``coinduced_compose`` と ``induced_compose`` を参照）．本書では， ``TopologicalSpace.coinduced f T`` に対して :math:`f_*T` ， ``TopologicalSpace.induced f T`` に対して :math:`f^*T` という表記を使用します．
 BOTH: -/
 #check coinduced_compose
 
@@ -420,7 +420,7 @@ each point has a basis of closed neighborhoods.
 
 OMIT. -/
 /- TEXT:
-位相空間の圏には非常に優れた性質があることを見てきました．その代償として，かなり病的な位相空間が存在します．位相空間には，その振る舞いが距離空間の振る舞いに近くなるようにするための仮定がいくつか存在します．最も重要なものは ``T2Space`` で，これは「ハウスドルフ性」とも呼ばれ，極限が一意であることを保証します．より強力な分離特性は ``T3Space`` で，これは `RegularSpace` の特性に加えて，各店が閉近傍の基底を持つことを保証します．
+位相空間の圏には非常に優れた性質があることを見てきました．その代償として，かなり病的な位相空間が存在します．位相空間には，その振る舞いが距離空間の振る舞いに近くなるようにするための仮定がいくつか存在します．最も重要なものは ``T2Space`` で，これは「ハウスドルフ性」とも呼ばれ，極限が一意であることを保証します．より強力な分離特性は ``T3Space`` で，これは `RegularSpace` の特性に加えて，各点が閉近傍の基底を持つことを保証します．
 BOTH: -/
 -- QUOTE:
 example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a))
@@ -559,7 +559,7 @@ Because we know ``Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y))`` this implies
 
 OMIT. -/
 /- TEXT:
-まず ``φ`` が連続であることを証明しましょう．任意の ``x : X`` を固定します． ``Y`` は正則であるので， ``φ x`` の *閉* 近傍 ``V'`` に対して， ``φ ⁻¹' V' ∈ 𝓝 x`` が成り立つことを確認すれば十分です．極限の仮定は（上の補助的な補題によって） ``IsOpen V ∧ (↑) ⁻¹' V ⊆ f ⁻¹' V'`` を満たす ``V ∈ 𝓝 x`` を与えます． ``V ∈ 𝓝 x`` であるため， ``V ⊆ φ ⁻¹' V'`` ，すなわち  ``∀ y ∈ V, φ y ∈ V'`` を証明すれば十分です．ここで ``V`` の要素 ``y`` を固定しましょう． ``V`` は *開* であるため， ``y`` の近傍です．特に ``(↑) ⁻¹' V ∈ comap (↑) (𝓝 y)`` となり，また ``f ⁻¹' V' ∈ comap (↑) (𝓝 y)`` となります．さらに ``A`` は稠密であるため， ``comap (↑) (𝓝 y) ≠ ⊥`` です．そして ``Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y))`` は既知であるため， ``φ y ∈ closure V'`` が導かれ， ``V'`` が閉じていることから ``φ y ∈ V'`` が証明されたことになります．
+まず ``φ`` が連続であることを証明しましょう．任意の ``x : X`` を固定します． ``Y`` は正則であるので， ``φ x`` の **閉** 近傍 ``V'`` に対して， ``φ ⁻¹' V' ∈ 𝓝 x`` が成り立つことを確認すれば十分です．極限の仮定は（上の補助的な補題によって） ``IsOpen V ∧ (↑) ⁻¹' V ⊆ f ⁻¹' V'`` を満たす ``V ∈ 𝓝 x`` を与えます． ``V ∈ 𝓝 x`` であるため， ``V ⊆ φ ⁻¹' V'`` ，すなわち  ``∀ y ∈ V, φ y ∈ V'`` を証明すれば十分です．ここで ``V`` の要素 ``y`` を固定しましょう． ``V`` は **開** であるため， ``y`` の近傍です．特に ``(↑) ⁻¹' V ∈ comap (↑) (𝓝 y)`` となり，また ``f ⁻¹' V' ∈ comap (↑) (𝓝 y)`` となります．さらに ``A`` は稠密であるため， ``comap (↑) (𝓝 y) ≠ ⊥`` です．そして ``Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y))`` は既知であるため， ``φ y ∈ closure V'`` が導かれ， ``V'`` が閉じていることから ``φ y ∈ V'`` が証明されたことになります．
 
 TEXT. -/
 /- OMIT:
@@ -654,7 +654,7 @@ ie such that ``F ≤ 𝓟 s``, has a cluster point in ``s``.
 
 OMIT. -/
 /- TEXT:
-したがって，集合 ``s`` は， ``s`` に含まれるすべての空でない一般化された集合 ``F`` ，つまり ``F ≤ 𝓟 s`` が ``s`` にクラスター点を持つとき，コンパクトであると言うことができます．
+したがって，集合 ``s`` は， ``s`` に含まれるすべての空でない一般化された集合 ``F`` ，つまり ``F ≤ 𝓟 s`` が ``s`` に集積点を持つとき，コンパクトであると言うことができます．
 
 BOTH: -/
 -- QUOTE: