From 2757c78e35509ad9021380a2cfed3e0f11e7af05 Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Mon, 22 Apr 2024 16:46:12 -0500 Subject: [PATCH] another typo --- MIL/C09_Topology/S03_Topological_Spaces.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/MIL/C09_Topology/S03_Topological_Spaces.lean b/MIL/C09_Topology/S03_Topological_Spaces.lean index 1c4241af..e4f2cd0d 100644 --- a/MIL/C09_Topology/S03_Topological_Spaces.lean +++ b/MIL/C09_Topology/S03_Topological_Spaces.lean @@ -382,8 +382,8 @@ In addition ``comap (↑) (𝓝 y) ≠ ⊥`` because ``A`` is dense. Because we know ``Tendsto f (comap (↑) (𝓝 y)) (𝓝 (φ y))`` this implies ``φ y ∈ closure V'`` and, since ``V'`` is closed, we have proved ``φ y ∈ V'``. -It remains to prove that ``φ`` extends ``f``. This is were continuity of ``f`` enters the discussion, -together with the fact that ``Y`` is Hausdorff. +It remains to prove that ``φ`` extends ``f``. This is where the continuity of ``f`` enters the +discussion, together with the fact that ``Y`` is Hausdorff. BOTH: -/ -- QUOTE: example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X}