.. _topology:

.. index:: topology

위상수학
========

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

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

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

이전 장들은 여러분에게 익숙했을 법한 수학적 개념들에 의존했지만, 필터의 개념은 많은 현업 수학자들에게조차 잘 알려져 있지 않습니다. 그러나 이 개념은 수학을 효과적으로 형식화하는 데 필수적입니다. 그 이유를 설명해 보겠습니다. ``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``\ 가 ``+∞``\ 로 향한다고 말하고 싶을 수 있습니다. 이로써 예순네 가지 서로 다른 종류의 극한 명제가 생기는데, :numref:`sequences_and_convergence`\ 에서 다뤘던 수열의 극한은 아직 다루기 시작하지도 않았습니다.

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

.. include:: C11_Topology/S01_Filters.inc
.. include:: C11_Topology/S02_Metric_Spaces.inc
.. include:: C11_Topology/S03_Topological_Spaces.inc