11. 위상수학

미적분학은 함수라는 개념에 기초하며, 함수는 서로 의존하는 양을 모델링하는 데 사용됩니다. 예를 들어, 시간에 따라 변하는 양을 연구하는 일은 흔합니다. 극한이라는 개념 또한 기본적입니다. \(x\)가 값 \(a\)에 다가갈 때 함수 \(f(x)\)의 극한이 값 \(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를 유리수 값으로 제한하거나 정의역에 다른 제약을 둘 수도 있지만, 여기서는 이 8가지 경우만 다룹시다.

공역에서도 비슷하게 다양한 선택지가 있습니다. f x가 어떤 값에 왼쪽이나 오른쪽에서 다가간다거나, 양의 무한대나 음의 무한대로 간다는 식으로 지정할 수 있습니다. 예를 들어 x가 x₀와 같아지지 않으면서 오른쪽에서 x₀로 갈 때 f x가 +∞로 간다고 말하고 싶을 수 있습니다. 이렇게 하면 서로 다른 종류의 극한 명제가 64가지나 생기는데, 제 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를 포함하는 모든 집합으로 이루어진 이른바 주 필터(principal filter)를 대응시킬 수 있습니다. 이 정의는 이미 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 ℕ을 정의해 보십시오. (ℕ 대신 준순서가 있는 어떤 타입이든 사용할 수 있습니다.)

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에 연관된 푸시포워드 연산 \(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도 있습니다. 이 연산은 집합에 대한 역상 연산을 일반화합니다. 임의의 사상 f에 대해 Filter.map f와 Filter.comap f는 갈루아 연결(Galois connection)이라고 알려진 관계를 이룹니다. 즉, 다음을 만족합니다.

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

이는 모든 F와 G에 대해 성립합니다. 이 연산을 사용하면 Tendsto를 다르게 정식화할 수 있으며, 이 정식화는 Mathlib의 정의와 (정의상으로는 아니지만) 증명을 통해 동치임을 보일 수 있습니다.

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

곱 연산은 당김 연산과 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를 정의할 수 있습니다. 또한 전제 조건 없이 당김 연산을 정의할 수도 있습니다. 실제로 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 절에서 정의한 수렴 개념보다 더 강하다고 느껴질 수 있습니다. 일반적인 정의는 표준 근방 Ioo (x₀ - ε) (x₀ + ε)에 대해서만 이를 요구하는 반면, 여기서는 x₀의 모든 근방의 역상이 atTop에 속할 것을 요구하기 때문입니다. 핵심은 정의에 의해 모든 근방이 그러한 표준 근방을 하나 포함한다는 점입니다. 이 관찰로부터 필터 기저라는 개념이 나옵니다.

F : Filter X가 주어졌을 때, 모든 집합 U에 대해 U ∈ F인 것과 U가 어떤 s i를 포함하는 것이 동치이면 집합족 s : ι → Set X를 F의 기저라고 합니다. 다시 말해 형식적으로 표현하면, s가 ∀ U : Set X, U ∈ F ↔ ∃ i, s i ⊆ U를 만족하면 s는 기저입니다. 인덱스 타입의 값 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 norm)을 선택하므로 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.comp이며, 이는 Continuous 네임스페이스에 있으므로 점 표기법을 사용하여 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를 결합하는 방식은 위에서처럼 점 표기법을 적극 활용하더라도 투박하게 느껴집니다. 더 심각한 문제는 이 멋진 증명을 작성하려면 사전에 많은 계획이 필요하다는 점입니다. 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의 엘러보레이터는 합성을 인식하지 못하고 이 보조정리의 적용을 거부합니다. 엘러보레이터는 타입의 곱이 관련된 경우에 특히 이 부분에 취약합니다.

여기서 적용하기에 더 좋은 보조정리는 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을 사용하는 것이며, 그 결과는 다음과 같습니다

엘러보레이션에 더 유리한 버전과 입력하기에 더 짧은 버전 중 하나를 골라야 하는 것은 아쉬운 일이므로, Continuous.fst'가 제공하는 마지막 압축으로 이 논의를 마무리합시다. 이를 사용하면 hf.comp continuous_fst를 hf.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. 균등 연속 함수

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

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은 컴팩트 공간들의 곱이 컴팩트하다는 것을 알고 있으므로 K는 컴팩트합니다.

그런 다음 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\)를 위상 공간, \(A\)를 \(X\)의 조밀한 부분집합, \(f : A → Y\)를 \(A\)에서 \(T_3\) 공간 \(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\)로 수렴한다”는 가정은 당김(pull-back) 필터 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의 확장임을 증명하는 일이 남았습니다. 바로 여기서 Y가 하우스도르프 공간이라는 사실과 함께 f의 연속성이 논의에 등장합니다.

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가 주어졌을 때, F를 일반화된 집합으로 보았을 때 x에 가까운 점들의 일반화된 집합과의 교집합이 공집합이 아니면, 점 x : X를 F의 집적점이라고 합니다.

그러면 s에 포함된, 즉 F ≤ 𝓟 s를 만족하는 공집합이 아닌 모든 일반화된 집합 F가 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가 map u atTop, 즉 매우 큰 자연수들의 일반화된 집합인 atTop의 u : ℕ → X에 의한 상이라면, 가정 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를 덮는 유한 부분족을 가지면 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