11. 위상수학

미적분학은 함수라는 개념에 기초하며, 함수는 서로 의존하는 양들을 모형화하는 데 사용됩니다. 예를 들어, 시간에 따라 변화하는 양들을 연구하는 것은 흔한 일입니다. 극한이라는 개념 또한 근본적입니다. 함수 \(f(x)\)의 극한은 \(x\)가 \(a\)에 접근할 때 \(b\)라는 값이라고 말하거나, \(x\)가 \(a\)에 접근할 때 \(f(x)\)가 \(b\)로 수렴한다고 말할 수 있습니다. 동등하게, \(x\)가 값 \(a\)에 접근함에 따라 \(f(x)\)가 \(b\)에 접근한다고 말할 수도 있고, 혹은 \(x\)가 \(a\)로 향함에 따라 그것이 \(b\)로 향한다고 말할 수도 있습니다. 우리는 제 3.6 절에서 이러한 개념들을 이미 다루기 시작했습니다.

위상수학은 극한과 연속성에 대한 추상적인 연구입니다. 형식화의 핵심 내용을 2장부터 7장까지 다뤘으므로, 이 장에서는 위상적 개념이 Mathlib에서 어떻게 형식화되는지 설명하겠습니다. 위상적 추상화는 훨씬 더 큰 일반성에 적용될 뿐만 아니라, 다소 역설적이게도 구체적인 사례에서 극한과 연속성에 대해 추론하기 쉽게 만들어 줍니다.

위상적 개념들은 상당히 많은 층의 수학적 구조 위에 세워집니다. 첫 번째 계층은 Chapter 4에서 설명한 것처럼 소박한 집합론입니다. 다음 계층은 필터의 이론이며, 이는 제 11.1 절에서 다룰 것입니다. 그 위에 우리는 위상 공간, 거리 공간, 그리고 균등 공간이라 불리는 다소 특이한 중간 개념의 이론들을 쌓습니다.

이전 장들은 여러분에게 익숙했을 법한 수학적 개념들에 의존했지만, 필터의 개념은 많은 현업 수학자들에게조차 잘 알려져 있지 않습니다. 그러나 이 개념은 수학을 효과적으로 형식화하는 데 필수적입니다. 그 이유를 설명해 보겠습니다. f : ℝ → ℝ를 임의의 함수라고 합시다. x가 어떤 값 x₀에 접근할 때 f x의 극한을 생각할 수 있지만, x가 무한대나 음의 무한대에 접근할 때 f x의 극한을 생각할 수도 있습니다. 더 나아가, x가 오른쪽에서 x₀에 접근할 때(관습적으로 x₀⁺로 표기)나 왼쪽에서 접근할 때(x₀⁻로 표기)의 f x의 극한도 생각할 수 있습니다. x가 x₀, x₀⁺, 또는 x₀⁻에 접근하지만 값 x₀ 자체는 취할 수 없는 변형들도 있습니다. 이로써 x가 무언가에 접근하는 방식은 적어도 여덟 가지가 됩니다. x의 값을 유리수로 제한하거나 정의역에 다른 제약을 둘 수도 있지만, 이 여덟 가지 경우로 한정하겠습니다.

공역에서도 이와 비슷하게 다양한 선택지가 있습니다: f x가 왼쪽이나 오른쪽에서 어떤 값에 접근한다고 명시하거나, 양의 무한대나 음의 무한대에 접근한다고 명시하는 등입니다. 예를 들어 x가 x₀와 같지 않으면서 오른쪽에서 x₀에 접근할 때 f x가 +∞로 향한다고 말하고 싶을 수 있습니다. 이로써 예순네 가지 서로 다른 종류의 극한 명제가 생기는데, 제 3.6 절에서 다뤘던 수열의 극한은 아직 다루기 시작하지도 않았습니다.

문제는 뒷받침하는 보조정리에 이르러서는 훨씬 더 복잡해집니다. 예를 들어, 극한은 합성됩니다: x가 x₀로 향할 때 f x가 y₀로 향하고, y가 y₀로 향할 때 g y가 z₀로 향하면, x가 x₀로 향할 때 g ∘ f x는 z₀로 향합니다. 여기에는 “향한다”라는 개념이 세 가지 작용하며, 각각은 앞 단락에서 설명한 여덟 가지 방식 중 어느 것으로도 구체화될 수 있습니다. 이로 인해 512개의 보조정리가 생기는데, 라이브러리에 추가해야 할 것치고는 너무 많은 양입니다! 비형식적으로는, 수학자들은 대개 이 중 두세 개만 증명하고 나머지는 “같은 방식으로” 증명될 수 있다고 언급하는 데 그칩니다. 수학을 형식화하려면 여기서 말하는 “같음”이라는 개념을 완전히 명시적으로 만들어야 하는데, 부르바키의 필터 이론이 바로 이를 해냅니다.

11.1. 필터

타입 X 위의 필터란 아래에서 자세히 설명할 세 가지 조건을 만족하는 X의 집합들의 모임입니다. 이 개념은 서로 연관된 두 가지 아이디어를 뒷받침합니다:

  • 극한: 앞서 논의한 모든 종류의 극한, 즉 수열의 유한 및 무한 극한, 한 점 또는 무한대에서의 함수의 유한 및 무한 극한 등을 포함합니다.

  • 결국 일어나는 일들: 충분히 큰 n : ℕ에 대해 일어나는 일, 점 x에 충분히 가까운 곳에서 일어나는 일, 충분히 가까운 점들의 쌍에 대해 일어나는 일, 또는 측도론적 의미에서 거의 모든 곳에서 일어나는 일 등을 포함합니다. 쌍대적으로, 필터는 자주 일어나는 일이라는 개념도 표현할 수 있습니다. 예를 들어, 임의로 큰 n에 대해, 또는 주어진 점의 임의의 근방 안의 한 점에서 등이 있습니다.

이러한 설명에 대응하는 필터들은 이 절의 뒷부분에서 정의하겠지만, 지금 미리 이름을 붙여볼 수 있습니다:

  • (atTop : Filter ℕ)는 어떤 N에 대해 {n | n ≥ N}을 포함하는 ℕ의 집합들로 이루어집니다

  • 𝓝 x는 위상 공간에서 x의 근방들로 이루어집니다

  • 𝓤 X는 균등 공간의 근접 영역(entourage)들로 이루어집니다(균등 공간은 거리 공간과 위상군을 일반화한 것입니다)

  • μ.ae는 측도 μ에 대해 여집합의 측도가 0인 집합들로 이루어집니다.

일반적인 정의는 다음과 같습니다: 필터 F : Filter X는 다음을 만족하는 집합들의 모음 F.sets : Set (Set X)입니다:

  • F.univ_sets : univ ∈ F.sets

  • F.sets_of_superset : ∀ {U V}, U ∈ F.sets → U ⊆ V → V ∈ F.sets

  • F.inter_sets : ∀ {U V}, U ∈ F.sets → V ∈ F.sets → U ∩ V ∈ F.sets.

첫 번째 조건은 X의 모든 원소로 이루어진 집합이 F.sets에 속한다는 것을 말합니다. 두 번째 조건은 U가 F.sets에 속하면 U를 포함하는 것은 무엇이든 F.sets에도 속한다는 것을 말합니다. 세 번째 조건은 F.sets가 유한 교집합에 대해 닫혀 있다는 것을 말합니다. Mathlib에서 필터 F는 F.sets와 그 세 가지 성질을 묶은 구조체로 정의되지만, 그 성질들은 추가적인 데이터를 담고 있지 않으므로 F와 F.sets의 구분을 흐리는 것이 편리합니다. 따라서 우리는 U ∈ F를 U ∈ F.sets를 의미하는 것으로 정의합니다. 이는 U ∈ F를 언급하는 일부 보조정리의 이름에 sets라는 단어가 등장하는 이유를 설명합니다.

필터를 “충분히 큰” 집합이라는 개념을 정의하는 것으로 생각하면 도움이 될 수 있습니다. 그러면 첫 번째 조건은 univ가 충분히 크다는 것을 말하고, 두 번째 조건은 충분히 큰 집합을 포함하는 집합은 충분히 크다는 것을 말하며, 세 번째 조건은 충분히 큰 두 집합의 교집합이 충분히 크다는 것을 말합니다.

타입 X에 대한 필터를 Set X의 일반화된 원소로 생각하는 것이 훨씬 더 유용할 수 있습니다. 예를 들어, atTop은 “매우 큰 수들의 집합”이고 𝓝 x₀는 “x₀에 매우 가까운 점들의 집합”입니다. 이러한 관점의 한 표현은 임의의 s : Set X에 대해 s를 포함하는 모든 집합으로 이루어진, 이른바 주 필터를 대응시킬 수 있다는 것입니다. 이 정의는 이미 Mathlib에 있으며 (Filter 네임스페이스에 지역화된) 표기법 𝓟를 가지고 있습니다. 시연을 위해, 이 기회를 활용하여 여기서 정의를 직접 작성해 보시기 바랍니다.

def principal {α : Type*} (s : Set α) : Filter α
    where
  sets := { t | s ⊆ t }
  univ_sets := sorry
  sets_of_superset := sorry
  inter_sets := sorry

두 번째 예제로, 필터 atTop : Filter ℕ을 정의해 보시기 바랍니다. (ℕ 대신 선순서(preorder)가 있는 임의의 타입을 사용할 수 있습니다.)

example : Filter ℕ :=
  { sets := { s | ∃ a, ∀ b, a ≤ b → b ∈ s }
    univ_sets := sorry
    sets_of_superset := sorry
    inter_sets := sorry }

또한 임의의 x : ℝ의 근방들의 필터 𝓝 x를 직접 정의할 수도 있습니다. 실수에서 x의 근방은 열린 구간 \((x_0 - \varepsilon, x_0 + \varepsilon)\)을 포함하는 집합이며, 이는 Mathlib에서 Ioo (x₀ - ε) (x₀ + ε)로 정의됩니다. (이 근방 개념은 Mathlib에 있는 더 일반적인 구성의 특수한 경우일 뿐입니다.)

이 예제들을 통해, 함수 f : X → Y가 어떤 F : Filter X를 따라 어떤 G : Filter Y로 수렴한다는 것이 무엇을 의미하는지 다음과 같이 이미 정의할 수 있습니다.

def Tendsto₁ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :=
  ∀ V ∈ G, f ⁻¹' V ∈ F

X가 ℕ이고 Y가 ℝ일 때, Tendsto₁ u atTop (𝓝 x)는 수열 u : ℕ → ℝ가 실수 x로 수렴한다는 말과 동치입니다. X와 Y가 모두 ℝ일 때, Tendsto f (𝓝 x₀) (𝓝 y₀)는 익숙한 개념인 \(\lim_{x \to x₀} f(x) = y₀\)와 동치입니다. 서론에서 언급한 다른 모든 종류의 극한들 또한, 정의역과 공역에 대한 적절한 필터 선택에 따른 Tendsto₁의 인스턴스와 동치입니다.

위의 Tendsto₁ 개념은 Mathlib에서 정의된 Tendsto 개념과 정의상 동치이지만, 후자가 더 추상적으로 정의되어 있습니다. Tendsto₁의 정의에 있는 문제는 한정사와 G의 원소들을 노출한다는 점이며, 필터를 일반화된 집합으로 보는 것에서 얻는 직관을 감춘다는 점입니다. 더 대수적이고 집합론적인 도구를 사용하여 한정사 ∀ V를 감추고 직관을 더 두드러지게 만들 수 있습니다. 첫 번째 구성 요소는 임의의 함수 f : X → Y에 연관된 pushforward 연산 \(f_*\)이며, Mathlib에서는 Filter.map f로 표기됩니다. X 위의 필터 F가 주어졌을 때, Filter.map f F : Filter Y는 V ∈ Filter.map f F ↔ f ⁻¹' V ∈ F가 정의상 성립하도록 정의됩니다. 예제 파일에서는 Filter.map을 map으로 쓸 수 있도록 Filter 네임스페이스를 열어 두었습니다. 이는 Filter Y 위의 순서 관계, 즉 원소 집합의 포함 관계를 뒤집은 것을 사용하여 Tendsto의 정의를 다시 쓸 수 있음을 의미합니다. 다시 말해, G H : Filter Y가 주어졌을 때, G ≤ H ↔ ∀ V : Set Y, V ∈ H → V ∈ G가 성립합니다.

def Tendsto₂ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :=
  map f F ≤ G

example {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) :
    Tendsto₂ f F G ↔ Tendsto₁ f F G :=
  Iff.rfl

필터에 대한 순서 관계가 거꾸로인 것처럼 보일 수 있습니다. 그러나 임의의 집합 s를 대응하는 주필터로 보내는 포함 사상 𝓟 : Set X → Filter X를 통해, X 위의 필터를 Set X의 일반화된 원소로 볼 수 있다는 점을 상기하십시오. 이 포함 사상은 순서를 보존하므로, Filter에 대한 순서 관계는 실제로 일반화된 집합들 사이의 자연스러운 포함 관계로 볼 수 있습니다. 이 유비에서 푸시포워드(pushforward)는 직접상(direct image)에 대응됩니다. 그리고 실제로 map f (𝓟 s) = 𝓟 (f '' s)입니다.

이제 우리는 수열 u : ℕ → ℝ가 점 x₀로 수렴하는 것이 map u atTop ≤ 𝓝 x₀인 것과 동치인 이유를 직관적으로 이해할 수 있습니다. 이 부등식은 “매우 큰 자연수들의 집합”의 “u에 의한 직접상”이 “x₀에 매우 가까운 점들의 집합”에 “포함”됨을 의미합니다.

약속했던 대로, Tendsto₂의 정의에는 어떠한 한정기호나 집합도 나타나지 않습니다. 이는 또한 푸시포워드 연산의 대수적 성질을 활용합니다. 첫째, 각 Filter.map f는 단조입니다. 둘째, Filter.map은 합성과 호환됩니다.

#check (@Filter.map_mono : ∀ {α β} {m : α → β}, Monotone (map m))

#check
  (@Filter.map_map :
    ∀ {α β γ} {f : Filter α} {m : α → β} {m' : β → γ}, map m' (map m f) = map (m' ∘ m) f)

이 두 성질을 함께 사용하면 극한이 합성됨을 증명할 수 있으며, 서론에서 설명한 합성 보조정리의 512가지 변형 모두와 그 이상을 한 번에 얻을 수 있습니다. Tendsto₁을 전칭 기호로 정의한 것과 대수적 정의 중 하나를, 위의 두 보조정리와 함께 사용하여 다음 명제를 증명하는 연습을 할 수 있습니다.

example {X Y Z : Type*} {F : Filter X} {G : Filter Y} {H : Filter Z} {f : X → Y} {g : Y → Z}
    (hf : Tendsto₁ f F G) (hg : Tendsto₁ g G H) : Tendsto₁ (g ∘ f) F H :=
  sorry

푸시포워드(pushforward) 구성은 함수를 사용하여 필터를 함수의 정의역에서 공역으로 밀어냅니다. 다른 방향으로 가는 풀백( Filter.comap ) 연산도 있습니다. 이는 집합의 원상(preimage) 연산을 일반화한 것입니다. 임의의 사상 f 에 대해, Filter.map f 와 Filter.comap f 는 갈루아 연결이라고 알려진 것을 형성하는데, 이는 다음을 만족한다는 뜻입니다

Filter.map_le_iff_le_comap : Filter.map f F ≤ G ↔ F ≤ Filter.comap f G

모든 F와 G에 대해서 말입니다. 이 연산은 Mathlib의 것과 (정의상으로는 아니지만) 증명 가능하게 동치인 Tendsto의 또 다른 공식화를 제공하는 데 사용될 수 있습니다.

comap 연산은 필터를 부분 타입으로 제한하는 데 사용될 수 있습니다. 예를 들어 f : ℝ → ℝ, x₀ : ℝ, y₀ : ℝ가 있고, x가 유리수 안에서 x₀에 접근할 때 f x가 y₀에 접근한다고 서술하고 싶다고 합시다. 강제 변환 함수 (↑) : ℚ → ℝ를 사용하여 필터 𝓝 x₀를 ℚ로 끌어올 수 있으며, Tendsto (f ∘ (↑) : ℚ → ℝ) (comap (↑) (𝓝 x₀)) (𝓝 y₀)라고 서술할 수 있습니다.

variable (f : ℝ → ℝ) (x₀ y₀ : ℝ)

#check comap ((↑) : ℚ → ℝ) (𝓝 x₀)

#check Tendsto (f ∘ (↑)) (comap ((↑) : ℚ → ℝ) (𝓝 x₀)) (𝓝 y₀)

당김 연산은 합성과도 호환되지만, 반변적이며, 이는 곧 인자의 순서를 뒤집는다는 것을 의미합니다.

section
variable {α β γ : Type*} (F : Filter α) {m : γ → β} {n : β → α}

#check (comap_comap : comap m (comap n F) = comap (n ∘ m) F)

end

이제 평면 ℝ × ℝ로 주의를 돌려, 점 (x₀, y₀)의 근방이 𝓝 x₀ 및 𝓝 y₀와 어떻게 관련되는지 이해해 봅시다. 곱 연산 Filter.prod : Filter X → Filter Y → Filter (X × Y)가 있으며, 이는 ×ˢ로 표기되고, 이 질문에 답합니다:

example : 𝓝 (x₀, y₀) = 𝓝 x₀ ×ˢ 𝓝 y₀ :=
  nhds_prod_eq

곱 연산은 pullback 연산과 inf 연산으로 정의됩니다:

F ×ˢ G = (comap Prod.fst F) ⊓ (comap Prod.snd G)입니다.

여기서 inf 연산은 임의의 타입 X에 대한 Filter X위의 격자 구조를 가리키며, F ⊓ G는 F와 G 모두보다 작은 필터 중 가장 큰 필터입니다. 따라서 inf 연산은 집합의 교집합 개념을 일반화합니다.

Mathlib의 많은 증명은 앞서 언급한 구조(map, comap, inf, sup, prod)를 모두 사용하여, 필터의 원소를 전혀 참조하지 않고도 수렴에 대한 대수적 증명을 제공합니다. 다음 보조정리의 증명에서 이를 연습할 수 있으며, 필요하다면 Tendsto와 Filter.prod의 정의를 펼치십시오.

#check le_inf_iff

example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) :
    Tendsto f atTop (𝓝 (x₀, y₀)) ↔
      Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) :=
  sorry

순서 타입 Filter X는 실제로 완비 격자입니다. 즉, 최소 원소가 존재하고, 최대 원소가 존재하며, X위의 모든 필터 집합은 Inf와 Sup를 가집니다.

필터의 정의에서 두 번째 성질(U가 F에 속하면 U보다 큰 것도 모두 F에 속함)이 주어지면, 첫 번째 성질(X의 모든 원소로 이루어진 집합이 F에 속함)은 F가 공집합들의 모음이 아니라는 성질과 동치라는 점에 유의하십시오. 이는 공집합이 F의 원소인지에 관한 더 미묘한 문제와 혼동해서는 안 됩니다. 필터의 정의는 ∅ ∈ F를 금지하지 않지만, 공집합이 F에 속하면 모든 집합이 F에 속하는데, 이는 곧 ∀ U : Set X, U ∈ F임을 뜻합니다. 이 경우 F는 다소 자명한 필터이며, 이는 정확히 완비 격자 Filter X의 최소 원소입니다. 이는 공집합을 포함하는 필터를 허용하지 않는 Bourbaki의 필터 정의와 대조됩니다.

정의에 자명한 필터를 포함시켰기 때문에, 일부 보조정리에서는 비자명성을 명시적으로 가정해야 하는 경우가 있습니다. 하지만 그 대가로 이론은 더 나은 전역적 성질을 갖게 됩니다. 자명한 필터를 포함시키면 최소 원소를 얻게 된다는 것을 이미 살펴보았습니다. 또한 이는 공집합을 배제하는 전제 조건을 추가하지 않고도 ∅를 ⊥로 대응시키는 principal : Set X → Filter X를 정의할 수 있게 해 줍니다. 그리고 이는 전제 조건 없이도 당김(pullback) 연산을 정의할 수 있게 해 줍니다. 실제로 F ≠ ⊥이더라도 comap f F = ⊥이 될 수 있습니다. 예를 들어, x₀ : ℝ와 s : Set ℝ가 주어졌을 때, s에 대응하는 부분 타입으로부터의 강제 변환에 의한 𝓝 x₀의 당김은, x₀가 s의 폐포에 속할 때만 비자명합니다.

어떤 필터가 자명하지 않다고 가정해야 하는 보조정리를 다루기 위해, Mathlib은 Filter.NeBot이라는 타입 클래스를 가지고 있으며, 라이브러리에는 (F : Filter X) [F.NeBot]을 가정하는 보조정리들이 있습니다. 인스턴스 데이터베이스는 예를 들어 (atTop : Filter ℕ).NeBot임을 알고 있으며, 자명하지 않은 필터를 밀어내면(push forward) 자명하지 않은 필터가 된다는 사실도 알고 있습니다. 그 결과, [F.NeBot]을 가정하는 보조정리는 임의의 수열 u에 대해 map u atTop에 자동으로 적용됩니다.

필터의 대수적 성질과 극한과의 관계에 대한 우리의 탐구는 본질적으로 끝났지만, 통상적인 극한 개념을 되찾았다는 우리의 주장을 아직 정당화하지 않았습니다. 표면적으로는 Tendsto u atTop (𝓝 x₀)가 제 3.6 절에서 정의된 수렴 개념보다 더 강한 것처럼 보일 수 있는데, 우리는 x₀의 모든 근방이 atTop에 속하는 원상을 가진다고 요구하는 반면, 통상적인 정의는 표준 근방 Ioo (x₀ - ε) (x₀ + ε)에 대해서만 이를 요구하기 때문입니다. 핵심은 정의에 따라 모든 근방이 그러한 표준 근방을 포함한다는 것입니다. 이 관찰은 필터 기저라는 개념으로 이어집니다.

F : Filter X가 주어졌을 때, 집합족 s : ι → Set X가 F의 기저라는 것은, 모든 집합 U에 대해 U ∈ F인 것과 어떤 s i를 포함하는 것이 동치임을 의미합니다. 달리 말해, 형식적으로 표현하면 s가 ∀ U : Set X, U ∈ F ↔ ∃ i, s i ⊆ U를 만족할 때 기저라고 합니다. 인덱싱 타입에서 값 i 중 일부만을 선택하는 ι에 대한 술어(predicate)를 고려하면 훨씬 더 유연합니다. 𝓝 x₀의 경우, ι를 ℝ로 두고, i를 ε로 표기하며, 술어는 ε의 양수 값들을 선택해야 합니다. 따라서 집합 Ioo  (x₀ - ε) (x₀ + ε)가 ℝ 위의 근방 위상에 대한 기저를 이룬다는 사실은 다음과 같이 서술됩니다:

example (x₀ : ℝ) : HasBasis (𝓝 x₀) (fun ε : ℝ ↦ 0 < ε) fun ε ↦ Ioo (x₀ - ε) (x₀ + ε) :=
  nhds_basis_Ioo_pos x₀

필터 atTop에 대한 좋은 기저도 있습니다. 보조정리 Filter.HasBasis.tendsto_iff는 F와 G의 기저가 주어졌을 때 Tendsto f F G 형태의 명제를 재구성할 수 있게 해줍니다. 이러한 요소들을 종합하면 제 3.6 절에서 사용했던 수렴 개념을 본질적으로 얻게 됩니다.

example (u : ℕ → ℝ) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ∈ Ioo (x₀ - ε) (x₀ + ε) := by
  have : atTop.HasBasis (fun _ : ℕ ↦ True) Ici := atTop_basis
  rw [this.tendsto_iff (nhds_basis_Ioo_pos x₀)]
  simp

이제 필터가 충분히 큰 수에 대해 성립하는 성질이나 주어진 점에 충분히 가까운 점들에 대해 성립하는 성질을 다루는 작업을 어떻게 용이하게 하는지 보이겠습니다. 앞서 제 3.6 절에서는 어떤 성질 P n이 충분히 큰 n에 대해 성립하고 Q n도 충분히 큰 n에 대해 성립하는 상황을 자주 마주했습니다. cases를 두 번 사용하면 ∀ n ≥ N_P, P n과 ∀ n ≥ N_Q, Q n을 만족하는 N_P와 N_Q를 얻을 수 있었습니다. set N := max N_P N_Q를 사용하면 결국 ∀ n ≥ N, P n ∧ Q n을 증명할 수 있었습니다. 이 작업을 반복하는 것은 지루한 일이 됩니다.

“충분히 큰 n에 대해 P n과 Q n이 성립한다”는 명제는 {n | P n} ∈ atTop이고 {n | Q n} ∈ atTop임을 의미한다는 점에 주목하면 더 잘 할 수 있습니다. atTop이 필터라는 사실은 atTop의 두 원소의 교집합이 다시 atTop에 속함을 함의하므로, {n | P n ∧ Q n} ∈ atTop임을 얻습니다. {n | P n} ∈ atTop라고 쓰는 것은 보기 불편하지만, 더 시사적인 표기법인 ∀ᶠ n in atTop, P n을 사용할 수 있습니다. 여기서 위첨자로 붙은 f는 “필터(Filter)”를 뜻합니다. 이 표기법은 “충분히 큰 수들의 집합”에 속하는 모든 n에 대해 P n이 성립한다고 말하는 것으로 생각할 수 있습니다. ∀ᶠ 표기법은 Filter.Eventually를 의미하며, 보조정리 Filter.Eventually.and는 필터의 교집합 성질을 이용해 방금 설명한 것을 수행합니다:

example (P Q : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) :
    ∀ᶠ n in atTop, P n ∧ Q n :=
  hP.and hQ

이 표기법은 매우 편리하고 직관적이어서, P가 등식이나 부등식 명제인 경우에 대한 특수화도 마련되어 있습니다. 예를 들어 u와 v를 두 실수 수열이라 하고, 충분히 큰 n에 대해 u n과 v n이 일치하면 u가 x₀로 수렴하는 것과 v가 x₀로 수렴하는 것이 동치임을 보여봅시다. 먼저 일반적인 Eventually를 사용하고, 그다음 등식 술어에 특화된 EventuallyEq를 사용하겠습니다. 두 명제는 정의상 동치이므로 두 경우 모두 같은 증명이 통합니다.

example (u v : ℕ → ℝ) (h : ∀ᶠ n in atTop, u n = v n) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) :=
  tendsto_congr' h

example (u v : ℕ → ℝ) (h : u =ᶠ[atTop] v) (x₀ : ℝ) :
    Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) :=
  tendsto_congr' h

Eventually의 관점에서 필터의 정의를 다시 살펴보는 것은 유익합니다. F : Filter X가 주어졌을 때, X 위의 임의의 술어 P와 Q에 대해,

  • 조건 univ ∈ F는 (∀ x, P x) → ∀ᶠ x in F, P x를 보장하며,

  • 조건 U ∈ F → U ⊆ V → V ∈ F는 (∀ᶠ x in F, P x) → (∀ x, P x → Q x) → ∀ᶠ x in F, Q x를 보장하며,

  • 조건 U ∈ F → V ∈ F → U ∩ V ∈ F는 (∀ᶠ x in F, P x) → (∀ᶠ x in F, Q x) → ∀ᶠ x in F, P x ∧ Q x를 보장합니다.

#check Eventually.of_forall
#check Eventually.mono
#check Eventually.and

Eventually.mono에 해당하는 두 번째 항목은 필터를 사용하는 좋은 방법을 제공하며, 특히 Eventually.and와 결합될 때 그러합니다. filter_upwards 택틱을 사용하면 이들을 결합할 수 있습니다. 비교해 보십시오:

example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
    (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by
  apply (hP.and (hQ.and hR)).mono
  rintro n ⟨h, h', h''⟩
  exact h'' ⟨h, h'⟩

example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
    (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by
  filter_upwards [hP, hQ, hR] with n h h' h''
  exact h'' ⟨h, h'⟩

측도론을 아는 독자라면 여집합의 측도가 0인 집합들의 필터 μ.ae (즉 “거의 모든 점으로 이루어진 집합”)가 Tendsto의 출발점이나 도착점으로는 그다지 유용하지 않지만, Eventually와 함께 사용하면 어떤 성질이 거의 모든 점에서 성립한다는 것을 편리하게 표현할 수 있다는 점에 주목할 것입니다.

∀ᶠ x in F, P x에는 때때로 유용한 쌍대 버전이 있습니다: ∃ᶠ x in F, P x는 {x | ¬P x} ∉ F를 의미합니다. 예를 들어 ∃ᶠ n in atTop, P n은 P n이 성립하는 임의로 큰 n이 존재함을 의미합니다. ∃ᶠ 표기법은 Filter.Frequently를 나타냅니다.

더 정교한 예로, 수열 u, 집합 M, 값 x에 대한 다음 명제를 살펴봅시다:

u가 x로 수렴하고 충분히 큰 n에 대해 u n이 M에 속한다면, x는 M의 폐포에 속합니다.

이는 다음과 같이 형식화할 수 있습니다:

Tendsto u atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M.

이는 위상 라이브러리에 있는 정리 mem_closure_of_tendsto의 특수한 경우입니다. 인용된 보조정리들을 사용하여 증명할 수 있는지 확인해 보십시오. 이때 ClusterPt x F가 (𝓝 x ⊓ F).NeBot을 의미한다는 사실과, 정의상 가정 ∀ᶠ n in atTop, u n ∈ M이 M ∈ map u atTop을 의미한다는 사실을 활용하십시오.

#check mem_closure_iff_clusterPt
#check le_principal_iff
#check neBot_of_le

example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
    (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M :=
  sorry

11.2. 거리 공간

이전 절의 예제들은 실수의 수열에 초점을 맞추고 있습니다. 이 절에서는 일반성을 조금 높여서 거리 공간에 초점을 맞추겠습니다. 거리 공간은 거리 함수 dist : X → X → ℝ를 갖춘 타입 X이며, 이는 X = ℝ인 경우의 함수 fun x y ↦ |x - y|를 일반화한 것입니다.

이러한 공간을 도입하는 것은 쉬우며, 거리 함수에 필요한 모든 성질을 확인해 보겠습니다.

variable {X : Type*} [MetricSpace X] (a b c : X)

#check (dist a b : ℝ)
#check (dist_nonneg : 0 ≤ dist a b)
#check (dist_eq_zero : dist a b = 0 ↔ a = b)
#check (dist_comm a b : dist a b = dist b a)
#check (dist_triangle a b c : dist a c ≤ dist a b + dist b c)

거리가 무한할 수 있거나, a = b가 아니어도 dist a b가 0이 될 수 있는 변형, 또는 둘 다 해당하는 변형도 있다는 점에 유의하십시오. 이들은 각각 EMetricSpace, PseudoMetricSpace, PseudoEMetricSpace라고 불립니다(여기서 “e”는 “extended”를 의미합니다).

ℝ에서 거리 공간으로 이어지는 우리의 여정이 선형대수학도 필요로 하는 노름 공간이라는 특수한 경우를 건너뛰었다는 점에 유의하십시오. 이는 미적분학 장의 일부로 설명될 것입니다.

11.2.1. 수렴과 연속성

거리 함수를 사용하면 이미 수렴하는 수열과 거리 공간 사이의 연속 함수를 정의할 수 있습니다. 이들은 실제로는 다음 절에서 다룰 더 일반적인 설정에서 정의되지만, 그 정의를 거리로 다시 표현하는 보조정리들이 있습니다.

example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  Metric.tendsto_atTop

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} :
    Continuous f ↔
      ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε :=
  Metric.continuous_iff

많은 보조정리에 몇 가지 연속성 가정이 있어서, 결국 우리는 많은 연속성 결과를 증명하게 되며, 이 작업을 전담하는 continuity 택틱이 있습니다. 아래 연습문제에서 필요할 연속성 명제를 증명해 봅시다. Lean이 두 거리 공간의 곱을 거리 공간으로 다루는 방법을 알고 있다는 점에 주목하십시오. Lean은 sup 노름을 선택하므로, dist (x₁, y₁) (x₂, y₂) = max (dist x₁ x₂) (dist y₁ y₂)는 반사성에 의해 성립합니다. 그 결과, X × X에서 ℝ로 가는 연속 함수를 고려하는 것이 타당합니다. 특히 (커리되지 않은 버전의) 거리 함수가 바로 그러한 함수입니다.

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by continuity

이 택틱은 다소 느리므로, 손으로 직접 하는 방법을 아는 것도 유용합니다. 먼저 fun p : X × X ↦ f p.1이 연속임을 사용해야 하는데, 이는 가정 hf에 의해 연속인 f와, 그 연속성이 보조정리 continuous_fst의 내용인 사영 prod.fst의 합성이기 때문입니다. 합성 성질은 Continuous 네임스페이스에 있는 Continuous.comp이므로, 점 표기법을 사용하여 Continuous.comp hf continuous_fst를 hf.comp continuous_fst로 압축할 수 있는데, 이는 실제로 우리의 가정과 보조정리를 합성하는 것으로 읽히기 때문에 오히려 더 읽기 쉽습니다. 두 번째 성분에 대해서도 같은 방법으로 fun p : X × X ↦ f p.2의 연속성을 얻을 수 있습니다. 그런 다음 이 두 연속성을 Continuous.prod_mk를 사용하여 조합하여 (hf.comp continuous_fst).prod_mk (hf.comp continuous_snd) : Continuous (fun p : X × X ↦ (f p.1, f p.2))를 얻고, 한 번 더 합성하여 완전한 증명을 완성합니다.

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  continuous_dist.comp ((hf.comp continuous_fst).prodMk (hf.comp continuous_snd))

Continuous.comp를 통해 Continuous.prod_mk와 continuous_dist를 결합하는 것은, 위에서처럼 점(dot) 표기법을 적극 활용하더라도 투박하게 느껴집니다. 더 심각한 문제는 이 훌륭한 증명이 많은 계획을 필요로 한다는 점입니다. Lean이 위 증명 항을 받아들이는 이유는, 그것이 우리 목표와 정의상 동등한 명제를 증명하는 완전한 항이기 때문이며, 여기서 풀어야 할 핵심 정의는 함수 합성의 정의입니다. 실제로 우리의 목표 함수 fun p : X × X ↦ dist (f p.1) (f p.2)는 합성으로 제시되어 있지 않습니다. 우리가 제시한 증명 항은 dist ∘ (fun p : X × X ↦ (f p.1, f p.2))의 연속성을 증명하는데, 이는 우리 목표 함수와 정의상 동일한 것으로 밝혀집니다. 하지만 apply continuous_dist.comp로 시작하는 택틱을 사용해 이 증명을 점진적으로 구성하려 하면, Lean의 정교화기(elaborator)는 합성을 인식하지 못하여 이 보조정리를 적용하기를 거부합니다. 타입의 곱(product)이 관련될 때 이 점이 특히 취약합니다.

여기서 적용하기 더 나은 보조정리는 Continuous.dist {f g : X → Y} : Continuous f → Continuous g → Continuous (fun x ↦ dist (f x) (g x))이며, 이는 Lean의 정교화기에 더 친화적일 뿐만 아니라 완전한 증명 항을 직접 제시할 때 더 짧은 증명을 제공하기도 하는데, 이는 위 명제에 대한 다음 두 가지 새로운 증명에서 확인할 수 있습니다.

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by
  apply Continuous.dist
  exact hf.comp continuous_fst
  exact hf.comp continuous_snd

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  (hf.comp continuous_fst).dist (hf.comp continuous_snd)

합성에서 비롯되는 정교화 문제가 없다면, 우리 증명을 압축하는 또 다른 방법은 때때로 유용한 Continuous.prod_map을 사용하는 것이며, 다음과 같이 됩니다.

정교화에 더 나은 버전과 입력하기 더 짧은 버전 중 하나를 선택해야 한다는 것은 아쉬운 일이므로, hf.comp continuous_fst를 hf.fst'로 압축할 수 있게 해주는 Continuous.fst'가 제공하는 마지막 압축으로 이 논의를 마무리하고(snd의 경우도 마찬가지입니다), 이제 난해함의 경계에 다다른 최종 증명을 얻어 봅시다.

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  hf.fst'.dist hf.snd'

이제 여러분이 연속성 보조정리를 증명할 차례입니다. continuity 택틱을 시도해 본 후, 직접 증명하려면 Continuous.add, continuous_pow, continuous_id가 필요할 것입니다.

example {f : ℝ → X} (hf : Continuous f) : Continuous fun x : ℝ ↦ f (x ^ 2 + x) :=
  sorry

지금까지는 연속성을 전역적인 개념으로 살펴보았지만, 한 점에서의 연속성도 정의할 수 있습니다.

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] (f : X → Y) (a : X) :
    ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε :=
  Metric.continuousAt_iff

11.2.2. 공, 열린집합과 닫힌집합

거리 함수가 있으면, 가장 중요한 기하학적 정의는 (열린) 공과 닫힌 공입니다.

variable (r : ℝ)

example : Metric.ball a r = { b | dist b a < r } :=
  rfl

example : Metric.closedBall a r = { b | dist b a ≤ r } :=
  rfl

여기서 r은 임의의 실수이며, 부호 제한이 없다는 점에 유의하십시오. 물론 일부 명제는 반지름 조건을 실제로 요구합니다.

example (hr : 0 < r) : a ∈ Metric.ball a r :=
  Metric.mem_ball_self hr

example (hr : 0 ≤ r) : a ∈ Metric.closedBall a r :=
  Metric.mem_closedBall_self hr

공이 있으면, 열린집합을 정의할 수 있습니다. 이는 사실 다음 절에서 다루는 더 일반적인 설정에서 정의되지만, 공을 이용해 정의를 다시 표현하는 보조정리가 있습니다.

example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.isOpen_iff

그러면 닫힌집합은 여집합이 열린집합인 집합입니다. 이들의 중요한 성질은 극한에 대해 닫혀 있다는 것입니다. 집합의 폐포는 그 집합을 포함하는 가장 작은 닫힌집합입니다.

example {s : Set X} : IsClosed s ↔ IsOpen (sᶜ) :=
  isOpen_compl_iff.symm

example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a))
    (hus : ∀ n, u n ∈ s) : a ∈ s :=
  hs.mem_of_tendsto hu (Eventually.of_forall hus)

example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε :=
  Metric.mem_closure_iff

mem_closure_iff_seq_limit을 사용하지 않고 다음 연습문제를 풀어 보십시오.

example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) :
    a ∈ closure s := by
  sorry

필터 절에서 근방 필터가 Mathlib에서 큰 역할을 한다는 것을 기억하십시오. 거리 공간 맥락에서 핵심은 공이 그러한 필터들의 기저를 제공한다는 점입니다. 여기서 주요 보조정리는 양의 반지름을 가진 열린 공과 닫힌 공에 대해 이를 주장하는 Metric.nhds_basis_ball과 Metric.nhds_basis_closedBall입니다. 중심점은 암묵적 인자이므로 다음 예제에서처럼 Filter.HasBasis.mem_iff를 호출할 수 있습니다.

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s :=
  Metric.nhds_basis_ball.mem_iff

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.closedBall x ε ⊆ s :=
  Metric.nhds_basis_closedBall.mem_iff

11.2.3. 컴팩트성

컴팩트성은 중요한 위상적 개념입니다. 이는 실수에서 선분이 다른 구간들과 비교했을 때 갖는 것과 같은 종류의 성질을 갖는 거리 공간의 부분집합을 구별합니다:

  • 컴팩트 집합에 값을 갖는 임의의 수열은 이 집합에서 수렴하는 부분수열을 갖습니다.

  • 실수에 값을 갖는 공집합이 아닌 컴팩트 집합 위의 임의의 연속 함수는 유계이며 어딘가에서 최댓값과 최솟값에 도달합니다(이를 극값 정리라고 부릅니다).

  • 컴팩트 집합은 닫힌 집합입니다.

먼저 실수에서 단위 구간이 실제로 컴팩트 집합인지 확인한 다음, 일반적인 거리 공간에서 컴팩트 집합에 대한 위 주장들을 확인해 봅시다. 두 번째 명제에서는 주어진 집합 위에서의 연속성만 필요하므로 Continuous 대신 ContinuousOn을 사용하며, 최솟값과 최댓값에 대해 별도의 명제를 제시하겠습니다. 물론 이 모든 결과는 더 일반적인 버전에서 유도되며, 그중 일부는 이후 절에서 다룰 것입니다.

example : IsCompact (Set.Icc 0 1 : Set ℝ) :=
  isCompact_Icc

example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) :
    ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) :=
  hs.tendsto_subseq hu

example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
      (hfs : ContinuousOn f s) :
    ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y :=
  hs.exists_isMinOn hs' hfs

example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
      (hfs : ContinuousOn f s) :
    ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x :=
  hs.exists_isMaxOn hs' hfs

example {s : Set X} (hs : IsCompact s) : IsClosed s :=
  hs.isClosed

추가로 Prop 값을 갖는 타입 클래스를 사용하여 거리 공간이 전역적으로 컴팩트하다고 명시할 수도 있습니다:

example {X : Type*} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X) :=
  isCompact_univ

컴팩트 거리 공간에서는 임의의 닫힌 집합이 컴팩트합니다. 이것이 바로 IsClosed.isCompact입니다.

11.2.4. 균등 연속 함수

이제 거리 공간에서의 균등성 개념, 즉 균등 연속 함수, 코시 수열, 완비성으로 넘어가겠습니다. 이들 역시 더 일반적인 맥락에서 정의되지만, Metric 이름공간에는 그 기본적인 정의에 접근할 수 있는 보조정리들이 있습니다. 먼저 균등 연속성부터 시작하겠습니다.

example {X : Type*} [MetricSpace X] {Y : Type*} [MetricSpace Y] {f : X → Y} :
    UniformContinuous f ↔
      ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε :=
  Metric.uniformContinuous_iff

이 모든 정의를 다루는 연습을 위해, 컴팩트 거리 공간에서 거리 공간으로 가는 연속 함수는 균등 연속임을 증명하겠습니다(더 일반적인 버전은 이후 절에서 살펴보겠습니다).

먼저 비형식적인 개요를 제시하겠습니다. f : X → Y를 컴팩트 거리 공간에서 거리 공간으로 가는 연속 함수라고 합시다. ε > 0을 고정하고 어떤 δ를 찾기 시작합니다.

φ : X × X → ℝ := fun p ↦ dist (f p.1) (f p.2)라 하고 K := { p : X × X | ε ≤ φ p }라 합시다. f와 거리 함수가 연속이므로 φ가 연속임을 관찰하십시오. 그리고 K는 명백히 닫혀 있으며(isClosed_le를 사용), X가 컴팩트하고 Lean은 컴팩트 공간의 곱이 컴팩트임을 알고 있으므로 컴팩트합니다.

그런 다음 eq_empty_or_nonempty를 사용하여 두 가지 가능성을 논의합니다. K가 공집합이면 명백히 끝난 것입니다(예를 들어 δ = 1로 설정할 수 있습니다). 그러므로 K가 공집합이 아니라고 가정하고, 최대·최소값 정리를 사용하여 K 위에서 거리 함수의 하한을 달성하는 (x₀, x₁)을 선택합시다. 그러면 δ = dist x₀ x₁로 집합을 설정하고 모든 것이 제대로 작동하는지 확인할 수 있습니다.

example {X : Type*} [MetricSpace X] [CompactSpace X]
      {Y : Type*} [MetricSpace Y] {f : X → Y}
    (hf : Continuous f) : UniformContinuous f := by
  sorry

11.2.5. 완비성

거리 공간에서의 코시 수열은 그 항들이 서로 점점 더 가까워지는 수열입니다. 이 개념을 표현하는 몇 가지 동치인 방법이 있습니다. 특히 수렴하는 수열은 코시 수열입니다. 그 역은 이른바 완비 공간에서만 성립합니다.

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε :=
  Metric.cauchySeq_iff

example (u : ℕ → X) :
    CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε :=
  Metric.cauchySeq_iff'

example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) :
    ∃ x, Tendsto u atTop (𝓝 x) :=
  cauchySeq_tendsto_of_complete hu

Mathlib에 등장하는 어떤 기준의 특수한 경우인 유용한 기준을 증명함으로써, 이 정의를 사용하는 연습을 해보겠습니다. 이는 또한 기하학적 맥락에서 큰 합을 사용하는 연습을 할 좋은 기회이기도 합니다. 필터 절에서의 설명에 더하여, 아마도 tendsto_pow_atTop_nhds_zero_of_lt_one, Tendsto.mul, dist_le_range_sum_dist가 필요할 것입니다.

theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
    (hu : ∀ n : ℕ, dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n) : CauchySeq u := by
  rw [Metric.cauchySeq_iff']
  intro ε ε_pos
  obtain ⟨N, hN⟩ : ∃ N : ℕ, 1 / 2 ^ N * 2 < ε := by sorry
  use N
  intro n hn
  obtain ⟨k, rfl : n = N + k⟩ := le_iff_exists_add.mp hn
  calc
    dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
    _ ≤ ∑ i  ∈ range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
    _ ≤ ∑ i  ∈ range k, (1 / 2 : ℝ) ^ (N + i) := sorry
    _ = 1 / 2 ^ N * ∑ i  ∈ range k, (1 / 2 : ℝ) ^ i := sorry
    _ ≤ 1 / 2 ^ N * 2 := sorry
    _ < ε := sorry

우리는 이 절의 최종 보스, 즉 완비 거리 공간에 대한 베르 정리를 마주할 준비가 되었습니다! 아래의 증명 스켈레톤은 흥미로운 기법들을 보여줍니다. 이는 느낌표 변형의 choose 택틱을 사용하며(이 느낌표를 제거해 보는 실험을 해 보아야 합니다), 증명 중간에서 Nat.rec_on을 사용하여 귀납적으로 무언가를 정의하는 방법을 보여줍니다.

open Metric

example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) :
    Dense (⋂ n, f n) := by
  let B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
  have Bpos : ∀ n, 0 < B n
  sorry
  /- Translate the density assumption into two functions `center` and `radius` associating
    to any n, x, δ, δpos a center and a positive radius such that
    `closedBall center radius` is included both in `f n` and in `closedBall x δ`.
    We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/
  have :
    ∀ (n : ℕ) (x : X),
      ∀ δ > 0, ∃ y : X, ∃ r > 0, r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n :=
    by sorry
  choose! center radius Hpos HB Hball using this
  intro x
  rw [mem_closure_iff_nhds_basis nhds_basis_closedBall]
  intro ε εpos
  /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x`
    belonging to all `f n`. For this, we construct inductively a sequence
    `F n = (c n, r n)` such that the closed ball `closedBall (c n) (r n)` is included
    in the previous ball and in `f n`, and such that `r n` is small enough to ensure
    that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs
    to all the `f n`. -/
  let F : ℕ → X × ℝ := fun n ↦
    Nat.recOn n (Prod.mk x (min ε (B 0)))
      fun n p ↦ Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
  let c : ℕ → X := fun n ↦ (F n).1
  let r : ℕ → ℝ := fun n ↦ (F n).2
  have rpos : ∀ n, 0 < r n := by sorry
  have rB : ∀ n, r n ≤ B n := by sorry
  have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by
    sorry
  have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry
  have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist
  -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
  rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
  -- this point `y` will be the desired point. We will check that it belongs to all
  -- `f n` and to `ball x ε`.
  use y
  have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by sorry
  have yball : ∀ n, y ∈ closedBall (c n) (r n) := by sorry
  sorry

11.3. 위상 공간

11.3.1. 기초

이제 일반성을 한 단계 높여 위상 공간을 소개합니다. 위상 공간을 정의하는 두 가지 주요 방법을 살펴본 다음, 위상 공간의 범주가 거리 공간의 범주보다 훨씬 더 다루기 쉬운 성질을 가지는 이유를 설명하겠습니다. 여기서는 Mathlib의 범주론을 사용하지 않고, 다소 범주론적인 관점만을 취한다는 점에 유의하십시오.

거리 공간에서 위상 공간으로의 이행을 생각하는 첫 번째 방법은, 열린 집합의 개념(또는 이와 동치인 닫힌 집합의 개념)만을 기억한다는 것입니다. 이 관점에서 볼 때, 위상 공간이란 열린 집합이라 불리는 집합들의 모음을 갖춘 타입입니다. 이 모음은 아래에 제시된 여러 공리를 만족해야 합니다(이 모음은 다소 중복적이지만 이 점은 무시하겠습니다).

section
variable {X : Type*} [TopologicalSpace X]

example : IsOpen (univ : Set X) :=
  isOpen_univ

example : IsOpen (∅ : Set X) :=
  isOpen_empty

example {ι : Type*} {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) : IsOpen (⋃ i, s i) :=
  isOpen_iUnion hs

example {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) :
    IsOpen (⋂ i, s i) :=
  isOpen_iInter_of_finite hs

그러면 닫힌 집합은 여집합이 열린 집합인 집합으로 정의됩니다. 위상 공간 사이의 함수는, 열린 집합의 모든 원상이 열린 집합이면 (전역적으로) 연속입니다.

variable {Y : Type*} [TopologicalSpace Y]

example {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
  continuous_def

이 정의를 통해 우리는 이미, 거리 공간과 비교했을 때 위상 공간이 연속함수를 논하는 데 필요한 정보만을 기억한다는 것을 알 수 있습니다: 한 타입 위의 두 위상 구조가 같은 것은 오직 그것들이 같은 연속함수를 가질 때뿐입니다(실제로 항등 함수는 두 구조가 같은 열린 집합을 가질 때에만 양방향으로 연속입니다).

하지만 한 점에서의 연속성으로 넘어가자마자 열린집합에 기반한 접근법의 한계가 드러납니다. Mathlib에서는 위상 공간을 각 점 x에 붙은 근방 필터 𝓝 x를 갖춘 타입으로 생각하는 경우가 많습니다(대응하는 함수 X → Filter X는 뒤에서 설명할 특정 조건을 만족합니다). 필터 절에서 이러한 장치들이 서로 연관된 두 가지 역할을 한다는 것을 기억하십시오. 첫째, 𝓝 x는 x에 가까운 X의 점들의 일반화된 집합으로 볼 수 있습니다. 그리고 이는 임의의 술어 P : X → Prop에 대해, 이 술어가 x에 충분히 가까운 점들에서 성립한다고 말하는 방법을 제공하는 것으로도 볼 수 있습니다. f : X → Y가 x에서 연속임을 서술해 봅시다. 순전히 필터적인 방식은, x에 가까운 점들의 일반화된 집합이 f에 의해 상으로 보내진 것이 f x에 가까운 점들의 일반화된 집합에 포함된다고 말하는 것입니다. 이는 map f (𝓝 x) ≤ 𝓝 (f x) 또는 Tendsto f (𝓝 x) (𝓝 (f x))로 표현된다는 것을 기억하십시오.

example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) :=
  Iff.rfl

일반적인 집합으로 본 근방과 일반화된 집합으로 본 근방 필터를 모두 사용하여 표현할 수도 있습니다: “f x의 임의의 근방 U에 대해, x에 가까운 모든 점은 U로 보내집니다”. 증명이 이번에도 Iff.rfl이라는 점에 주목하십시오. 이 관점은 이전 관점과 정의상 동치입니다.

example {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U :=
  Iff.rfl

이제 한 관점에서 다른 관점으로 넘어가는 방법을 설명합니다. 열린집합의 관점에서, 𝓝 x의 원소들을 x를 포함하는 열린집합을 포함하는 집합들로 간단히 정의할 수 있습니다.

example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t :=
  mem_nhds_iff

반대 방향으로 가려면 𝓝 : X → Filter X가 위상의 근방 함수가 되기 위해 만족해야 하는 조건을 논의해야 합니다.

첫 번째 제약 조건은, 일반화된 집합으로 본 𝓝 x가 일반화된 집합 pure x로 본 집합 {x}를 포함한다는 것입니다(이 이상한 이름을 설명하는 것은 너무 곁길로 새는 일이므로, 지금은 그저 받아들이기로 합니다). 이를 달리 말하면, 어떤 술어가 x에 가까운 점들에 대해 성립한다면 x에서도 성립한다는 것입니다.

example (x : X) : pure x ≤ 𝓝 x :=
  pure_le_nhds x

example (x : X) (P : X → Prop) (h : ∀ᶠ y in 𝓝 x, P y) : P x :=
  h.self_of_nhds

그다음, 더 미묘한 요구 사항은, 임의의 술어 P : X → Prop와 임의의 x에 대해, x에 가까운 y에 대해 P y가 성립한다면, x에 가까운 y와 y에 가까운 z에 대해 P z가 성립한다는 것입니다. 더 정확히는 다음과 같습니다:

example {P : X → Prop} {x : X} (h : ∀ᶠ y in 𝓝 x, P y) : ∀ᶠ y in 𝓝 x, ∀ᶠ z in 𝓝 y, P z :=
  eventually_eventually_nhds.mpr h

이 두 결과는 X 위의 위상 공간 구조의 근방 함수인 X → Filter X 함수들을 특징짓습니다. 여전히 TopologicalSpace.mkOfNhds : (X → Filter X) → TopologicalSpace X 함수가 존재하지만, 이 함수는 입력이 위의 두 제약 조건을 만족할 때만 그 입력을 근방 함수로 되돌려줍니다. 더 정확히는, 이를 다른 방식으로 말해주는 보조정리 TopologicalSpace.nhds_mkOfNhds가 있으며, 다음 연습문제에서는 이 다른 방식을 우리가 위에서 서술한 방식으로부터 유도합니다.

example {α : Type*} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a)
    (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) :
    ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' := by
  sorry
end

TopologicalSpace.mkOfNhds는 그리 자주 사용되지는 않지만, 근방 필터가 정확히 어떤 의미에서 위상 공간 구조의 전부인지 알아두는 것은 여전히 유용합니다.

Mathlib에서 위상 공간을 효율적으로 사용하기 위해 알아야 할 다음 사항은, 우리가 TopologicalSpace : Type u → Type u의 형식적 성질을 많이 사용한다는 것입니다. 순수하게 수학적인 관점에서 볼 때, 이러한 형식적 성질들은 위상 공간이 거리 공간이 지닌 문제들을 어떻게 해결하는지 설명하는 매우 깔끔한 방법입니다. 이 관점에서 볼 때, 위상 공간이 해결하는 문제는 거리 공간이 함자성을 거의 갖지 못하고, 전반적으로 매우 나쁜 범주론적 성질을 갖는다는 점입니다. 이는 이미 논의한 바와 같이, 거리 공간이 위상적으로 무관한 기하학적 정보를 많이 담고 있다는 사실에 더해지는 것입니다.

먼저 함자성에 집중해 봅시다. 거리 공간 구조는 부분집합에 유도될 수 있고, 이는 단사 함수에 의해 당겨질 수 있다는 것과 동치입니다. 하지만 그것이 거의 전부입니다. 그것들은 일반적인 함수에 의해 당겨질 수도, 전사 함수에 의해서조차 밀어낼 수도 없습니다.

특히 거리 공간의 몫 공간이나 비가산 개의 거리 공간의 곱에는 합리적인 거리를 부여할 수 없습니다. 예를 들어 ℝ로 색인된 ℝ의 사본들의 곱으로 볼 수 있는 타입 ℝ → ℝ를 생각해 봅시다. 함수열의 점별 수렴이 그럴듯한 수렴 개념이라고 말하고 싶습니다. 하지만 이러한 수렴 개념을 부여하는 거리는 ℝ → ℝ에 존재하지 않습니다. 이와 관련하여, 사상 f : X → (ℝ → ℝ)가 연속인 것과 모든 t : ℝ에 대해 fun x ↦ f x t가 연속인 것이 동치가 되도록 보장하는 거리도 존재하지 않습니다.

이제 이러한 모든 문제를 해결하는 데 사용되는 자료를 살펴보겠습니다. 먼저 임의의 사상 f : X → Y를 사용하여 위상을 한쪽에서 다른 쪽으로 밀어내거나 끌어올 수 있습니다. 이 두 연산은 갈루아 연결을 이룹니다.

variable {X Y : Type*}

example (f : X → Y) : TopologicalSpace X → TopologicalSpace Y :=
  TopologicalSpace.coinduced f

example (f : X → Y) : TopologicalSpace Y → TopologicalSpace X :=
  TopologicalSpace.induced f

example (f : X → Y) (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) :
    TopologicalSpace.coinduced f T_X ≤ T_Y ↔ T_X ≤ TopologicalSpace.induced f T_Y :=
  coinduced_le_iff_le_induced

이러한 연산들은 함수의 합성과 호환됩니다. 평소와 같이, 밀어내기는 공변적이고 끌어오기는 반변적입니다. coinduced_compose와 induced_compose를 참고하십시오. 지면상으로는 TopologicalSpace.coinduced f T에 대해 \(f_*T\) 표기법을, TopologicalSpace.induced f T에 대해 \(f^*T\) 표기법을 사용하겠습니다.

그다음으로 큰 부분은 임의로 주어진 X에 대한 TopologicalSpace X의 완비 격자 구조입니다. 위상을 주로 열린집합의 데이터로 생각한다면, TopologicalSpace X의 순서 관계가 Set (Set X)에서 비롯되기를 기대할 것입니다. 즉, 집합 u가 t에 대해 열려 있으면 t'에 대해서도 열려 있어서 t ≤ t'이 성립하기를 기대합니다. 하지만 Mathlib은 열린집합보다 근방에 더 초점을 맞춘다는 것을 이미 알고 있으므로, 임의의 x : X에 대해 위상 공간에서 근방으로 가는 사상 fun T : TopologicalSpace X ↦ @nhds X T x가 순서를 보존하기를 원합니다. 또한 Filter X의 순서 관계는 principal : Set X → Filter X가 순서를 보존하도록 설계되어 있어, 필터를 일반화된 집합으로 볼 수 있게 해준다는 것을 알고 있습니다. 따라서 우리가 실제로 TopologicalSpace X에서 사용하는 순서 관계는 Set (Set X)에서 비롯되는 것과 반대입니다.

example {T T' : TopologicalSpace X} : T ≤ T' ↔ ∀ s, T'.IsOpen s → T.IsOpen s :=
  Iff.rfl

이제 push-forward(또는 pull-back) 연산과 순서 관계를 결합함으로써 연속성을 복원할 수 있습니다.

example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) :
    Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y :=
  continuous_iff_coinduced_le

이 정의와 push-forward와 합성의 호환성 덕분에, 임의의 위상 공간 \(Z\)에 대해 함수 \(g : Y → Z\)가 위상 \(f_*T_X\)에 대해 연속인 것과 \(g ∘ f\)가 연속인 것이 동치라는 보편적 성질을 거저 얻습니다.

\[\begin{split}g \text{ continuous } &⇔ g_*(f_*T_X) ≤ T_Z \\ &⇔ (g ∘ f)_* T_X ≤ T_Z \\ &⇔ g ∘ f \text{ continuous}\end{split}\]
example {Z : Type*} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z)
      (g : Y → Z) :
    @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔
      @Continuous X Z T_X T_Z (g ∘ f) := by
  rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le]

투영 사상을 f로 사용하여 이미 몫위상을 얻습니다. 이는 모든 X에 대해 TopologicalSpace X가 완비 격자라는 사실을 사용하지 않은 것입니다. 이제 이 모든 구조가 ‘추상적 헛소리(abstract nonsense)’만으로 곱위상의 존재를 어떻게 증명하는지 살펴봅시다. 위에서 ℝ → ℝ의 경우를 살펴보았지만, 이제 어떤 ι : Type*와 X : ι → Type*에 대한 Π i, X i의 일반적인 경우를 살펴봅시다. 임의의 위상 공간 Z와 임의의 함수 f : Z → Π i, X i에 대해, f가 연속인 것과 모든 i에 대해 (fun x ↦ x i) ∘ f가 연속인 것이 동치이기를 원합니다. 투영 (fun (x : Π i, X i) ↦ x i)에 대한 표기법 \(p_i\)를 사용하여 이 제약을 “종이 위에서” 탐구해 봅시다:

\[\begin{split}(∀ i, p_i ∘ f \text{ continuous}) &⇔ ∀ i, (p_i ∘ f)_* T_Z ≤ T_{X_i} \\ &⇔ ∀ i, (p_i)_* f_* T_Z ≤ T_{X_i}\\ &⇔ ∀ i, f_* T_Z ≤ (p_i)^*T_{X_i}\\ &⇔ f_* T_Z ≤ \inf \left[(p_i)^*T_{X_i}\right]\end{split}\]

그렇다면 Π i, X i 위에서 우리가 원하는 위상이 무엇인지 알 수 있습니다:

example (ι : Type*) (X : ι → Type*) (T_X : ∀ i, TopologicalSpace (X i)) :
    (Pi.topologicalSpace : TopologicalSpace (∀ i, X i)) =
      ⨅ i, TopologicalSpace.induced (fun x ↦ x i) (T_X i) :=
  rfl

이것으로 Mathlib이 위상 공간을 더 함자적인 이론으로 만들고 고정된 모든 타입에 대해 완비 격자 구조를 가지게 함으로써 거리 공간 이론의 결함을 어떻게 바로잡는다고 보는지에 대한 탐구를 마칩니다.

11.3.2. 분리성과 가산성

위상 공간의 범주가 매우 좋은 성질을 갖는다는 것을 살펴보았습니다. 이에 대한 대가는 다소 병적인 위상 공간이 존재한다는 것입니다. 위상 공간의 동작이 거리 공간의 동작에 더 가까워지도록 보장하기 위해 위상 공간에 부여할 수 있는 여러 가정이 있습니다. 가장 중요한 것은 “하우스도르프”라고도 불리는 T2Space로, 극한이 유일함을 보장합니다. 더 강한 분리 성질로는 T3Space가 있는데, 이는 추가로 RegularSpace 성질, 즉 각 점이 닫힌 근방의 기저를 가진다는 것을 보장합니다.

example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a))
    (hb : Tendsto u atTop (𝓝 b)) : a = b :=
  tendsto_nhds_unique ha hb

example [TopologicalSpace X] [RegularSpace X] (a : X) :
    (𝓝 a).HasBasis (fun s : Set X ↦ s ∈ 𝓝 a ∧ IsClosed s) id :=
  closed_nhds_basis a

정의에 따라, 모든 위상 공간에서 각 점은 열린 근방의 기저를 갖는다는 점에 유의하십시오.

example [TopologicalSpace X] {x : X} :
    (𝓝 x).HasBasis (fun t : Set X ↦ t ∈ 𝓝 x ∧ IsOpen t) id :=
  nhds_basis_opens' x

이제 우리의 주된 목표는 연속성에 의한 확장을 가능하게 하는 기본 정리를 증명하는 것입니다. 부르바키의 일반 위상수학 책 I.8.5, 정리 1에서 (자명하지 않은 함의만을 취함):

위상 공간 \(X\), \(X\)의 조밀한 부분집합 \(A\), 그리고 \(A\)에서 \(T_3\) 공간 \(Y\)로 가는 연속 사상 \(f : A → Y\)를 생각합시다. 만약 \(X\)의 각 \(x\)에 대해, \(y\)가 \(A\)에 속하면서 \(x\)로 수렴할 때 \(f(y)\)가 \(Y\)에서 극한을 가진다면, \(f\)를 \(X\)로 확장하는 연속 함수 \(φ\)가 존재합니다.

사실 Mathlib은 위 보조정리의 더 일반적인 버전인 IsDenseInducing.continuousAt_extend를 포함하고 있지만, 여기서는 부르바키의 버전을 고수하겠습니다.

A : Set X가 주어졌을 때 ↥A는 A에 연관된 부분 타입이며, Lean은 필요할 때 그 특이한 위쪽 화살표를 자동으로 삽입한다는 것을 기억하십시오. 그리고 (포함) 강제 변환 사상은 (↑) : A → X입니다. “A에 머무르면서 \(x\)로 수렴한다”는 가정은 풀백 필터 comap (↑) (𝓝 x)에 대응됩니다.

먼저 지역 문맥을 단순화하기 위해 추출된 보조정리를 증명해 봅시다(특히 여기서는 Y가 위상 공간일 필요가 없습니다).

theorem aux {X Y A : Type*} [TopologicalSpace X] {c : A → X}
      {f : A → Y} {x : X} {F : Filter Y}
      (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) :
    ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by
  sorry

이제 연속에 의한 확장 정리의 주요 증명으로 넘어가 봅시다.

Lean이 ↥A 위의 위상이 필요할 때는 자동으로 유도된 위상을 사용합니다. 유일하게 관련된 보조정리는 nhds_induced (↑) : ∀ a : ↥A, 𝓝 a = comap (↑) (𝓝 ↑a)입니다(사실 이는 유도된 위상에 대한 일반적인 보조정리입니다).

증명 개요는 다음과 같습니다:

주요 가정과 선택 공리는 ∀ x, Tendsto f (comap (↑) (𝓝 x)) (𝓝 (φ x))를 만족하는 함수 φ를 제공합니다(Y가 하우스도르프 공간이므로 φ는 완전히 결정되지만, φ가 실제로 f를 확장한다는 것을 증명하려고 시도하기 전까지는 이 사실이 필요하지 않습니다).

먼저 φ가 연속임을 증명해 봅시다. 임의의 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'임이 증명되었습니다.

이제 φ가 f를 확장함을 증명하는 일이 남았습니다. 바로 여기서 f의 연속성이, Y가 하우스도르프라는 사실과 함께 논의에 등장합니다.

example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X}
    (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f)
    (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) :
    ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by
  sorry

#check HasBasis.tendsto_right_iff

분리 성질 외에도, 위상 공간을 거리 공간에 더 가깝게 만들기 위해 가정할 수 있는 주요 가정의 종류는 가산성 가정입니다. 그 중 주된 것은 모든 점이 가산 근방 기저를 갖는다는 제1 가산성입니다. 특히 이는 집합의 폐포를 수열을 이용해 이해할 수 있도록 보장합니다.

example [TopologicalSpace X] [FirstCountableTopology X]
      {s : Set X} {a : X} :
    a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) :=
  mem_closure_iff_seq_limit

11.3.3. 콤팩트성

이제 위상 공간에서 콤팩트성이 어떻게 정의되는지 논의해 봅시다. 여느 때처럼 이를 생각하는 방법에는 여러 가지가 있으며, Mathlib은 필터 버전을 택합니다.

먼저 필터의 집적점을 정의해야 합니다. 위상 공간 X 위의 필터 F가 주어졌을 때, 점 x : X가 F의 집적점이라는 것은, F를 일반화된 집합으로 볼 때 x에 가까운 점들의 일반화된 집합과 공집합이 아닌 교집합을 갖는다는 것입니다.

그러면, s에 포함된 모든 공집합이 아닌 일반화된 집합 F, 즉 F ≤ 𝓟 s인 것이 s 안에 집적점을 가지면, 집합 s가 콤팩트하다고 말할 수 있습니다.

variable [TopologicalSpace X]

example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) :=
  Iff.rfl

example {s : Set X} :
    IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F :=
  Iff.rfl

예를 들어 F가 atTop, 즉 매우 큰 자연수들의 일반화된 집합의 u : ℕ → X에 의한 상인 map u atTop이라면, 가정 F ≤ 𝓟 s는 충분히 큰 n에 대해 u n이 s에 속한다는 것을 의미합니다. x가 map u atTop의 집적점이라는 것은, 매우 큰 수들의 상이 x에 가까운 점들의 집합과 교차한다는 것을 말합니다. 𝓝 x가 가산 기저를 갖는 경우, 이는 u가 x로 수렴하는 부분수열을 갖는다는 것으로 해석할 수 있으며, 이렇게 하면 거리 공간에서 콤팩트성이 어떤 모습인지를 다시 얻게 됩니다.

example [FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s)
    (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) :=
  hs.tendsto_subseq hu

집적점은 연속 함수와 잘 어울립니다.

variable [TopologicalSpace Y]

example {x : X} {F : Filter X} {G : Filter Y} (H : ClusterPt x F) {f : X → Y}
    (hfx : ContinuousAt f x) (hf : Tendsto f F G) : ClusterPt (f x) G :=
  ClusterPt.map H hfx hf

연습 문제로, 연속 사상에 의한 컴팩트 집합의 상이 컴팩트임을 증명해 보겠습니다. 이미 살펴본 내용에 더해, Filter.push_pull과 NeBot.of_map을 사용해야 합니다.

example {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) :
    IsCompact (f '' s) := by
  intro F F_ne F_le
  have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by sorry
  have Hne : (𝓟 s ⊓ comap f F).NeBot := by sorry
  have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left
  sorry

컴팩트성은 열린 덮개의 관점에서도 표현할 수 있습니다: s를 덮는 모든 열린 집합족이 유한한 덮개 부분족을 가지면 s는 컴팩트합니다.

example {ι : Type*} {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i))
    (hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i :=
  hs.elim_finite_subcover U hUo hsU