Lean-26 : Hommage à James R. Munkres — le cours 18.901 dans Mathlib 4

Navigation : Index | << Précédent | Série Lean

Hommage à James R. Munkres (1930-2026). Le MIT nous a quittés à l’été 2026 d’un mathématicien que les obituaires décrivent comme « Mathematician, musician and gardener ». Deux visages nous intéressent ici et dans les issues sœurs : le topologue — professeur au MIT de 1960 à 2000, il a enseigné son cours signature 18.901 Introduction to Topology jusqu’en 2015, et son manuel Topology (2e éd., 2000) reste LA référence mondiale du premier cours de topologie générale — et le musicien, honoré dans le volet 2/3 de cette série. Ce notebook honore le premier : il parcourt les notions du cours 18.901 telles qu’elles vivent aujourd’hui dans Mathlib.Topology.*, chaque concept interrogé par le compilateur Lean lui-même.

C’est le troisième volet d’une série hommage : 1/3 l’algorithme de Kuhn-Munkres (lake assignment_lean + GT-27), 2/3 le voice leading musical (Lean — non : notebook appli VoiceLeading, issue), 3/3 ce Tribute topologique. L’ordre est celui des vies de Munkres : l’algoriste (avec Kuhn), le musicien, le topologue.

Introduction : pourquoi Munkres dans une série Lean ?

James Raymond Munkres (1930-2026) a fait sa carrière au MIT, où sa recherche portait sur la topologie différentielle (son Elementary Differential Topology, 1966, est un classique du domaine). Mais c’est par son manuel d’enseignement qu’il a marqué des générations : Topology : A First Course (1975), devenu Topology (2e édition, 2000) — la porte d’entrée standard de la topologie générale, structurée autour des espaces topologiques, des axiomes de séparation, de la compacité et de la connexité. Le cours 18.901 qu’il a enseigné jusqu’en 2015 suit exactement ce fil.

Ce notebook fait ce que fait la série : interroger le concept directement dans Mathlib. Chaque section prend une notion du cours de Munkres, la déclare (#check), la met en théorème (example prouvé), et en certifie la provenance (#print axioms — les preuves de ce Tribute ne dépendent d’aucun axiome). Le notebook s’exécute avec le kernel lean4-wsl sur le lake mathlib_examples (toolchain v4.33.0) : toutes les sorties que vous voyez sont des sorties réelles du compilateur Lean.

Avertissement de vocabulaire : ne pas confondre avec la « topologie des jeux » (GameTheory-3-Topology2x2-Csharp.ipynb) — celle-là est la structure du graphe des issues d’un jeu, rien à voir avec la topologie générale de Munkres.

-- Toutes les importations de la session (tete de session, pattern Lean-24) :
-- les cinq chapitres du cours 18.901 + Closure pour les dualites adhérence/intérieur.
import Mathlib.Topology.Basic
import Mathlib.Topology.Continuous
import Mathlib.Topology.Separation.Hausdorff
import Mathlib.Topology.Compactness.Compact
import Mathlib.Topology.Connected.Basic
import Mathlib.Topology.Closure

-- Toutes les importations de la session (tete de session, pattern Lean-24) :

-- les cinq chapitres du cours 18.901 + Closure pour les dualites adhérence/intérieur.

import Mathlib.Topology.Basic

import Mathlib.Topology.Continuous

import Mathlib.Topology.Separation.Hausdorff

import Mathlib.Topology.Compactness.Compact

import Mathlib.Topology.Connected.Basic

import Mathlib.Topology.Closure

--% env 0

Raw input

{"cmd": "-- Toutes les importations de la session (tete de session, pattern Lean-24) :\n-- les cinq chapitres du cours 18.901 + Closure pour les dualites adh\u00e9rence/int\u00e9rieur.\nimport Mathlib.Topology.Basic\nimport Mathlib.Topology.Continuous\nimport Mathlib.Topology.Separation.Hausdorff\nimport Mathlib.Topology.Compactness.Compact\nimport Mathlib.Topology.Connected.Basic\nimport Mathlib.Topology.Closure"}

Raw output

{"env": 0}

1. Espaces topologiques : les trois axiomes

Le chapitre 2 de Munkres commence par la définition : une topologie sur un ensemble \(X\) est une collection \(\mathcal{T}\) de parties de \(X\) vérifiant trois axiomes — \(\emptyset\) et \(X\) sont ouverts, toute réunion d’ouverts est ouverte, toute intersection finie d’ouverts est ouverte. Dans Mathlib, TopologicalSpace X est une classe qui emballe exactement ces trois axiomes, et le prédicat IsOpen s (avec s : Set X) dit que \(s \in \mathcal{T}\).

-- Les trois axiomes de Munkres §12, tels que Mathlib les énonce.
variable {X : Type*} [TopologicalSpace X] {s t : Set X}

#check @TopologicalSpace          -- la classe : les trois axiomes emballés
#check @IsOpen                    -- s ∈ T
#check @isOpen_univ               -- axiome 1 : X est ouvert
#check @isOpen_empty              -- axiome 1 (bis) : ∅ est ouvert
#check @isOpen_iUnion             -- axiome 2 : réunion quelconque d'ouverts
#check @IsOpen.inter              -- axiome 3 : intersection finie (deux à deux)

-- Et ils s'utilisent : la preuve qui suit est une application directe des axiomes.
example (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∪ t) := hs.union ht
example (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t) := hs.inter ht

#print axioms IsOpen.union        -- certification : aucun axiome

-- Les trois axiomes de Munkres §12, tels que Mathlib les énonce.

variable {X : Type*} [TopologicalSpace X] {s t : Set X}

#check @TopologicalSpace          -- la classe : les trois axiomes emballés TopologicalSpace : Type u_2 → Type u_2

#check @IsOpen                    -- s ∈ T @IsOpen : {X : Type u_2} → [TopologicalSpace X] → Set X → Prop

#check @isOpen_univ               -- axiome 1 : X est ouvert @isOpen_univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsOpen Set.univ

#check @isOpen_empty              -- axiome 1 (bis) : ∅ est ouvert @isOpen_empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsOpen ∅

#check @isOpen_iUnion             -- axiome 2 : réunion quelconque d'ouverts @isOpen_iUnion : ∀ {X : Type u_2} {ι : Sort u_3} [inst : TopologicalSpace X] {f : ι → Set X},
  (∀ (i : ι), IsOpen (f i)) → IsOpen (⋃ i, f i)

#check @IsOpen.inter              -- axiome 3 : intersection finie (deux à deux) @IsOpen.inter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → IsOpen t → IsOpen (s ∩ t)

-- Et ils s'utilisent : la preuve qui suit est une application directe des axiomes.

example (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∪ t) := hs.union ht

example (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t) := hs.inter ht

#print axioms IsOpen.union        -- certification : aucun axiome 'IsOpen.union' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 1

Raw input

{"cmd": "-- Les trois axiomes de Munkres \u00a712, tels que Mathlib les \u00e9nonce.\nvariable {X : Type*} [TopologicalSpace X] {s t : Set X}\n\n#check @TopologicalSpace          -- la classe : les trois axiomes emball\u00e9s\n#check @IsOpen                    -- s \u2208 T\n#check @isOpen_univ               -- axiome 1 : X est ouvert\n#check @isOpen_empty              -- axiome 1 (bis) : \u2205 est ouvert\n#check @isOpen_iUnion             -- axiome 2 : r\u00e9union quelconque d'ouverts\n#check @IsOpen.inter              -- axiome 3 : intersection finie (deux \u00e0 deux)\n\n-- Et ils s'utilisent : la preuve qui suit est une application directe des axiomes.\nexample (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s \u222a t) := hs.union ht\nexample (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s \u2229 t) := hs.inter ht\n\n#print axioms IsOpen.union        -- certification : aucun axiome", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "TopologicalSpace : Type u_2 → Type u_2"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data": "@IsOpen : {X : Type u_2} → [TopologicalSpace X] → Set X → Prop"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "@isOpen_univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsOpen Set.univ"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@isOpen_empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsOpen ∅"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@isOpen_iUnion : ∀ {X : Type u_2} {ι : Sort u_3} [inst : TopologicalSpace X] {f : ι → Set X},\n  (∀ (i : ι), IsOpen (f i)) → IsOpen (⋃ i, f i)"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "@IsOpen.inter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → IsOpen t → IsOpen (s ∩ t)"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data":
   "'IsOpen.union' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 1}

Lecture. isOpen_iUnion porte la subtilité des axiomes de Munkres : la réunion est quelconque (indexée par un type ι arbitraire), alors que l’intersection n’est garantie que finie — IsOpen.inter est la version deux à deux, et c’est déjà tout ce que les axiomes donnent. Le contre-exemple classique (Munkres §13, ex. 1) : dans \(\mathbb{R}\), chaque singleton est fermé mais l’intersection dénombrable \(\bigcap_{n} (-1/n,\, 1/n) = \{0\}\)… est fermée — le bon contre-exemple est \(\bigcup\) vs \(\bigcap\) d’ouverts : \(\bigcap_{n} (-1/n, 1/n)\) est un singleton, pas ouvert, tandis que toute réunion d’ouverts l’est. C’est exactement cette asymétrie que portent les types de isOpen_iUnion (réunion sur ι quelconque) et IsOpen.inter (binaire seulement).

Pour aller plus loin — Surviving proofs, Counterexamples and Contradictions (12/09/2026) Sheydvasser, à l’article 2, recommande de chercher le contre-exemple canonique d’un théorème avant de se lancer dans une preuve. Ici, Munkres §13 ex. 1 — l’intersection dénombrable \(\bigcap_n (-1/n, 1/n) = \{0\}\) dans \(\mathbb{R}\) — est exactement ce contre-exemple canonique : il exhibe l’asymétrie entre réunion quelconque d’ouverts (toujours ouverte) et intersection dénombrable d’ouverts (pas nécessairement ouverte). Le type ι dans isOpen_iUnion porte cette asymétrie dans la signature même : la réunion est indexée par un type arbitraire, l’intersection est binaire (IsOpen.inter). C’est le geste que Sheydvasser défend à l’article 2 : un théorème sans son contre-exemple canonique n’est qu’à moitié compris — le contre-exemple révèle où l’énoncé cesse de tenir, et c’est précisément ce que l’asymétrie des types Mathlib formalise. Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/counterexamples-and-contradictions Archivé : G:DriveIA-Proves-Surviving-Proofs\2026-09-12_counterexamples-and-contradictions.html

2. Adhérence, intérieur, voisinages

Chapitre 2 toujours (§17-§19 chez Munkres) : l’intérieur de \(s\) est le plus grand ouvert contenu dans \(s\), l’adhérence le plus petit fermé le contenant, et un voisinage de \(x\) est une partie qui contient un ouvert contenant \(x\). Mathlib fait un choix caractéristique : le filtre des voisinages \(\mathcal{N}(x)\) (nhds x) est la notion primitive, et l’adhérence se définit à partir de lui — \(x \in \bar{s}\) ssi tout voisinage de \(x\) rencontre \(s\).

-- Adhérence, intérieur, voisinages : nhds est la primitive.
variable {X : Type*} [TopologicalSpace X] {s : Set X} {x : X}

#check @nhds                      -- le filtre des voisinages de x
#check @interior                  -- le plus grand ouvert contenu dans s
#check @closure                   -- le plus petit fermé contenant s
#check @mem_closure_iff_nhds_ne_bot  -- x ∈ s̄ ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥ (tout voisinage rencontre s)

-- Les dualités de Munkres §17, exercice 6 : intérieur et adhérence sont liés par passage au complémentaire.
example : interior sᶜ = (closure s)ᶜ := interior_compl
example : closure sᶜ = (interior s)ᶜ := closure_compl

#print axioms interior_compl      -- certification : aucun axiome

-- Adhérence, intérieur, voisinages : nhds est la primitive.

variable {X : Type*} [TopologicalSpace X] {s : Set X} {x : X}🟨 Variable name `s` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`

#check @nhds                      -- le filtre des voisinages de x @nhds : {X : Type u_3} → [TopologicalSpace X] → X → Filter X

#check @interior                  -- le plus grand ouvert contenu dans s @interior : {X : Type u_3} → [TopologicalSpace X] → Set X → Set X

#check @closure                   -- le plus petit fermé contenant s @closure : {X : Type u_3} → [TopologicalSpace X] → Set X → Set X

#check @mem_closure_iff_nhds_ne_bot  -- x ∈ s̄ ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥ (tout voisinage rencontre s) @mem_closure_iff_nhds_ne_bot : ∀ {X : Type u_3} [inst : TopologicalSpace X] {x : X} {s : Set X},
  x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥

-- Les dualités de Munkres §17, exercice 6 : intérieur et adhérence sont liés par passage au complémentaire.

example : interior sᶜ = (closure s)ᶜ := interior_compl

example : closure sᶜ = (interior s)ᶜ := closure_compl

#print axioms interior_compl      -- certification : aucun axiome 'interior_compl' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 2

Raw input

{"cmd": "-- Adh\u00e9rence, int\u00e9rieur, voisinages : nhds est la primitive.\nvariable {X : Type*} [TopologicalSpace X] {s : Set X} {x : X}\n\n#check @nhds                      -- le filtre des voisinages de x\n#check @interior                  -- le plus grand ouvert contenu dans s\n#check @closure                   -- le plus petit ferm\u00e9 contenant s\n#check @mem_closure_iff_nhds_ne_bot  -- x \u2208 s\u0304 \u2194 \ud835\udcdd x \u2293 \ud835\udcdf s \u2260 \u22a5 (tout voisinage rencontre s)\n\n-- Les dualit\u00e9s de Munkres \u00a717, exercice 6 : int\u00e9rieur et adh\u00e9rence sont li\u00e9s par passage au compl\u00e9mentaire.\nexample : interior s\u1d9c = (closure s)\u1d9c := interior_compl\nexample : closure s\u1d9c = (interior s)\u1d9c := closure_compl\n\n#print axioms interior_compl      -- certification : aucun axiome", "env": 1}

Raw output

{"messages":
 [{"severity": "warning",
   "pos": {"line": 2, "column": 48},
   "endPos": {"line": 2, "column": 49},
   "data":
   "Variable name `s` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "@nhds : {X : Type u_3} → [TopologicalSpace X] → X → Filter X"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data": "@interior : {X : Type u_3} → [TopologicalSpace X] → Set X → Set X"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data": "@closure : {X : Type u_3} → [TopologicalSpace X] → Set X → Set X"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@mem_closure_iff_nhds_ne_bot : ∀ {X : Type u_3} [inst : TopologicalSpace X] {x : X} {s : Set X},\n  x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥"},
  {"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data":
   "'interior_compl' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 2}

Lecture. La caractérisation mem_closure_iff_nhds_ne_bot est la formalisation littérale du « tout voisinage de \(x\) rencontre \(s\) » de Munkres §17 — exprimée dans le langage des filtres : le produit inférieur \(\mathcal{N}(x) \cap \mathcal{P}_s\) reste non trivial. Les deux dualités prouvées (interior_compl, closure_compl) sont exactement l’exercice 6 du §17 du manuel. Notez l’économie du point de vue filtre : adhérence, intérieur, limite de suites généralisées, tout s’exprime avec nhds — c’est le style Mathlib, plus économique que le style ensembliste du manuel mais démontrablement équivalent.

3. Continuité : la caractérisation par images réciproques

Le théorème central du chapitre 3 de Munkres (§18) : une fonction \(f : X \to Y\) est continue si et seulement si l’image réciproque de tout ouvert de \(Y\) est un ouvert de \(X\). C’est LA définition pratique — et c’est celle que Mathlib prend comme définition de Continuous.

-- Continuité : continuous_def EST le théorème de Munkres §18.1.
variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y}

#check @Continuous                -- la définition : preimage des ouverts ouverte
#check @continuous_def            -- explicitée en iff : ∀ s ouvert, IsOpen (f ⁻¹' s)

-- Deux exemples immédiats du manuel : l'identité, et les constantes.
example : Continuous (id : X → X) := continuous_id
example (y : Y) : Continuous (fun _ : X => y) := continuous_const

-- Et la preuve "à la main" directement depuis la définition :
example : Continuous (id : X → X) := continuous_def.2 fun s hs => hs

#print axioms continuous_def      -- certification : aucun axiome

-- Continuité : continuous_def EST le théorème de Munkres §18.1.

variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y}🟨 Variable name `s` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `s` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `t` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`

#check @Continuous                -- la définition : preimage des ouverts ouverte @Continuous : {X : Type u_5} → {Y : Type u_6} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop

#check @continuous_def            -- explicitée en iff : ∀ s ouvert, IsOpen (f ⁻¹' s) @continuous_def : ∀ {X : Type u_5} {Y : Type u_6} {x : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : X → Y},
  Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)

-- Deux exemples immédiats du manuel : l'identité, et les constantes.

example : Continuous (id : X → X) := continuous_id

example (y : Y) : Continuous (fun _ : X => y) := continuous_const

-- Et la preuve "à la main" directement depuis la définition :

example : Continuous (id : X → X) := continuous_def.2 fun s hs => hs🟨 Variable name `s` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`

#print axioms continuous_def      -- certification : aucun axiome 'continuous_def' does not depend on any axioms

--% env 3

Raw input

{"cmd": "-- Continuit\u00e9 : continuous_def EST le th\u00e9or\u00e8me de Munkres \u00a718.1.\nvariable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X \u2192 Y}\n\n#check @Continuous                -- la d\u00e9finition : preimage des ouverts ouverte\n#check @continuous_def            -- explicit\u00e9e en iff : \u2200 s ouvert, IsOpen (f \u207b\u00b9' s)\n\n-- Deux exemples imm\u00e9diats du manuel : l'identit\u00e9, et les constantes.\nexample : Continuous (id : X \u2192 X) := continuous_id\nexample (y : Y) : Continuous (fun _ : X => y) := continuous_const\n\n-- Et la preuve \"\u00e0 la main\" directement depuis la d\u00e9finition :\nexample : Continuous (id : X \u2192 X) := continuous_def.2 fun s hs => hs\n\n#print axioms continuous_def      -- certification : aucun axiome", "env": 2}

Raw output

{"messages":
 [{"severity": "warning",
   "pos": {"line": 2, "column": 37},
   "endPos": {"line": 2, "column": 38},
   "data":
   "Variable name `s` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 2, "column": 42},
   "endPos": {"line": 2, "column": 43},
   "data":
   "Variable name `s` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 2, "column": 44},
   "endPos": {"line": 2, "column": 45},
   "data":
   "Variable name `t` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "warning",
   "pos": {"line": 2, "column": 49},
   "endPos": {"line": 2, "column": 50},
   "data":
   "Variable name `x` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@Continuous : {X : Type u_5} → {Y : Type u_6} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@continuous_def : ∀ {X : Type u_5} {Y : Type u_6} {x : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : X → Y},\n  Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)"},
  {"severity": "warning",
   "pos": {"line": 12, "column": 58},
   "endPos": {"line": 12, "column": 59},
   "data":
   "Variable name `s` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
  {"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data": "'continuous_def' does not depend on any axioms"}],
 "env": 3}

Lecture. La seconde preuve de l’identité mérite une ligne : continuous_def.2 ouvre la caractérisation en « pour tout ouvert \(s\), montrer IsOpen (id ⁻¹' s) » — et id ⁻¹' s = s, donc l’hypothèse hs conclut. C’est le genre de preuve d’une ligne qui montre la définition au travail, exactement comme Munkres le demande dans les premières pages du §18. Le manuel prouve aussi l’équivalence avec la caractérisation par voisinages (§18 théorème 1, partie 2) — c’est continuous_iff_continuousAt dans Mathlib, même contenu, formulation filtre.

4. Séparation et compacité : T2 et l’axiome de Hausdorff

Chapitre 4 de Munkres : les axiomes de séparation (§17 pour \(T_1\), §31 pour la maison de Hausdorff \(T_2\) : deux points distincts admettent des voisinages disjoints) puis la compacité (§26 : tout recouvrement ouvert admet un sous-recouvrement fini). Deux propriétés que le cours 18.901 démontre dans cet ordre pour aboutir aux théorèmes pivots : compact + Hausdorff = normal, et le théorème de Tychonoff pour les produits.

-- Séparation et compacité.
variable {X : Type*} [TopologicalSpace X]

#check @T2Space                  -- la maison de Hausdorff : deux points distincts, voisinages disjoints
#check @t2_separation             --   la forme utilisable : x ≠ y → ∃ u v ouverts disjoints séparant x et y
#check @CompactSpace              -- tout recouvrement ouvert a un sous-recouvrement fini
#check @isCompact_univ            --   la forme ensembliste équivalente : IsCompact univ

-- La trivialité que Munkres fait démontrer en exercice : dans un espace compact, univ est... compact.
example [CompactSpace X] : IsCompact (Set.univ : Set X) := isCompact_univ

#print axioms isCompact_univ     -- certification : aucun axiome

-- Séparation et compacité.

variable {X : Type*} [TopologicalSpace X]

#check @T2Space                  -- la maison de Hausdorff : deux points distincts, voisinages disjoints T2Space : (X : Type u_6) → [TopologicalSpace X] → Prop

#check @t2_separation             --   la forme utilisable : x ≠ y → ∃ u v ouverts disjoints séparant x et y @t2_separation : ∀ {X : Type u_6} [inst : TopologicalSpace X] [T2Space X] {x y : X},
  x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

#check @CompactSpace              -- tout recouvrement ouvert a un sous-recouvrement fini CompactSpace : (X : Type u_6) → [TopologicalSpace X] → Prop

#check @isCompact_univ            --   la forme ensembliste équivalente : IsCompact univ @isCompact_univ : ∀ {X : Type u_6} [inst : TopologicalSpace X] [h : CompactSpace X], IsCompact Set.univ

-- La trivialité que Munkres fait démontrer en exercice : dans un espace compact, univ est... compact.

example [CompactSpace X] : IsCompact (Set.univ : Set X) := isCompact_univ

#print axioms isCompact_univ     -- certification : aucun axiome 'isCompact_univ' depends on axioms: [propext, Quot.sound]

--% env 4

Raw input

{"cmd": "-- S\u00e9paration et compacit\u00e9.\nvariable {X : Type*} [TopologicalSpace X]\n\n#check @T2Space                  -- la maison de Hausdorff : deux points distincts, voisinages disjoints\n#check @t2_separation             --   la forme utilisable : x \u2260 y \u2192 \u2203 u v ouverts disjoints s\u00e9parant x et y\n#check @CompactSpace              -- tout recouvrement ouvert a un sous-recouvrement fini\n#check @isCompact_univ            --   la forme ensembliste \u00e9quivalente : IsCompact univ\n\n-- La trivialit\u00e9 que Munkres fait d\u00e9montrer en exercice : dans un espace compact, univ est... compact.\nexample [CompactSpace X] : IsCompact (Set.univ : Set X) := isCompact_univ\n\n#print axioms isCompact_univ     -- certification : aucun axiome", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "T2Space : (X : Type u_6) → [TopologicalSpace X] → Prop"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@t2_separation : ∀ {X : Type u_6} [inst : TopologicalSpace X] [T2Space X] {x y : X},\n  x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data": "CompactSpace : (X : Type u_6) → [TopologicalSpace X] → Prop"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@isCompact_univ : ∀ {X : Type u_6} [inst : TopologicalSpace X] [h : CompactSpace X], IsCompact Set.univ"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data": "'isCompact_univ' depends on axioms: [propext, Quot.sound]"}],
 "env": 4}

Lecture. CompactSpace (la version « tout l’espace est compact ») et IsCompact s (la version par partie) sont deux faces de la même pièce — isCompact_univ_iff en fait une équivalence. Le choix de Mathlib de privilégier la classe CompactSpace reflète l’usage moderne (l’espace entier suffit à la plupart des énoncés), tandis que Munkres travaille dès le départ avec les parties. La définition formelle d’IsCompact via les filtres (« tout filtre contenant \(s\) a un point d’accumulation ») est à nouveau le style Mathlib : le §26 du manuel dit « tout recouvrement ouvert », et l’équivalence entre les deux formulations est un exercice classique que Mathlib a déjà absorbé dans ses définitions.

5. Connexité : l’intervalle et les corps

Dernier pilier du cours (Munkres §23-§25) : un espace est connexe s’il n’est pas réunion de deux ouverts non vides disjoints. Le théorème-phare du chapitre est l’irrationalité « structurelle » : les intervalles de \(\mathbb{R}\) sont connexes, donc l’image continue d’un intervalle est un intervalle (théorème des valeurs intermédiaires), donc \(\mathbb{Q}\) n’est pas connexe et \(\mathbb{R}\) l’est. Dans Mathlib, ConnectedSpace s’appuie sur IsConnected s (« \(s\) n’est pas réunion de deux ouverts non vides disjoints ») — la définition du manuel, mot pour mot.

-- Connexité.
variable {X : Type*} [TopologicalSpace X]

#check @ConnectedSpace           -- extends PreconnectedSpace : non vide + pas de séparation
#check @IsConnected              -- la version ensembliste : s ≠ ∅ et pas de clopen non trivial dans s
#check @isConnected_univ         -- ConnectedSpace ↔ IsConnected univ

example [ConnectedSpace X] : IsConnected (Set.univ : Set X) := isConnected_univ

#print axioms isConnected_univ   -- certification : aucun axiome

-- Connexité.

variable {X : Type*} [TopologicalSpace X]

#check @ConnectedSpace           -- extends PreconnectedSpace : non vide + pas de séparation ConnectedSpace : (α : Type u_7) → [TopologicalSpace α] → Prop

#check @IsConnected              -- la version ensembliste : s ≠ ∅ et pas de clopen non trivial dans s @IsConnected : {α : Type u_7} → [TopologicalSpace α] → Set α → Prop

#check @isConnected_univ         -- ConnectedSpace ↔ IsConnected univ @isConnected_univ : ∀ {α : Type u_7} [inst : TopologicalSpace α] [ConnectedSpace α], IsConnected Set.univ

example [ConnectedSpace X] : IsConnected (Set.univ : Set X) := isConnected_univ

#print axioms isConnected_univ   -- certification : aucun axiome 'isConnected_univ' does not depend on any axioms

--% env 5

Raw input

{"cmd": "-- Connexit\u00e9.\nvariable {X : Type*} [TopologicalSpace X]\n\n#check @ConnectedSpace           -- extends PreconnectedSpace : non vide + pas de s\u00e9paration\n#check @IsConnected              -- la version ensembliste : s \u2260 \u2205 et pas de clopen non trivial dans s\n#check @isConnected_univ         -- ConnectedSpace \u2194 IsConnected univ\n\nexample [ConnectedSpace X] : IsConnected (Set.univ : Set X) := isConnected_univ\n\n#print axioms isConnected_univ   -- certification : aucun axiome", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "ConnectedSpace : (α : Type u_7) → [TopologicalSpace α] → Prop"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@IsConnected : {α : Type u_7} → [TopologicalSpace α] → Set α → Prop"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "@isConnected_univ : ∀ {α : Type u_7} [inst : TopologicalSpace α] [ConnectedSpace α], IsConnected Set.univ"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "'isConnected_univ' does not depend on any axioms"}],
 "env": 5}

Lecture. Mathlib scinde la connexité en deux : PreconnectedSpace (pas de séparation par deux ouverts disjoints) et ConnectedSpace (qui ajoute la non-vacuité) — exactement la discussion de Munkres §23 sur la convention « connexe implique non vide ». La version ensembliste IsConnected est celle du manuel ; isConnected_univ fait le pont. Les grands théorèmes du chapitre (image continue d’un connexe, connexité de ℝ, des intervalles) vivent plus haut dans la hiérarchie (Mathlib.Topology.Connected.PathConnected, Mathlib.Topology.Instances.Real) et restent dans les chapitres suivants du cours — voir « pour aller plus loin ».

6. Ce qui est hors-scope de cet hommage

Le manuel de Munkres couvre bien plus que ces cinq chapitres — et la carrière de Munkres aussi. Sont hors scope de ce Tribute :

La topologie algébrique (groupe fondamental, revêtements — Munkres, Elements of Algebraic Topology, 1984) : la série à ce sujet vit dans le dépôt avec knot_lean et le notebook Lean-17a-Knots ;
Les variétés et l’analyse sur variétés (Analysis on Manifolds, 1991) — le Munkres topologue différentiel de Elementary Differential Topology (1966), un autre livre que le manuel général ;
La théorie de l’obstruction, son domaine de recherche propre — pas de formalisation dans Mathlib à ce jour.

Le lake dédié de topologie « à la Munkres » (identités adhérence/intérieur en lemmes nommés) est une phase 2 gated (issue #12600) : si la review du Tribute en montre le besoin, il viendra en PR séparée.

7. Exercices

Trois exercices dans l’esprit du manuel : appliquer les axiomes, utiliser la définition, prouver une dualité. Chaque cellule s’exécute telle quelle (la sortie du stub porte le marqueur declaration uses 'sorry') — à vous de remplacer le sorry par la vraie preuve, dont l’énoncé complet est dans le commentaire.

Exercice 1 — Réunion de trois ouverts

Les axiomes ne donnent l’union que deux à deux (IsOpen.union). Composez-les : si \(s\), \(t\) et \(u\) sont ouverts, alors \(s \cup t \cup u\) est ouvert. Indice : IsOpen.union prend deux arguments, et s ∪ t ∪ u est parenthésé (s ∪ t) ∪ u par associativité du ∪ de Lean.

-- Exercice 1 : réunion de trois ouverts.
-- TODO etudiant : remplacez sorry par la preuve (une application de IsOpen.union à deux reprises).
variable {X : Type*} [TopologicalSpace X] {s t u : Set X}

example (hs : IsOpen s) (ht : IsOpen t) (hu : IsOpen u) : IsOpen (s ∪ t ∪ u) := by
  sorry

-- Exercice 1 : réunion de trois ouverts.

-- TODO etudiant : remplacez sorry par la preuve (une application de IsOpen.union à deux reprises).

variable {X : Type*} [TopologicalSpace X] {s t u : Set X}

example (hs : IsOpen s) (ht : IsOpen t) (hu : IsOpen u) : IsOpen (s ∪ t ∪ u) := by🟨 declaration uses `sorry`

  sorry

--% env 6

--% prove 0

Raw input

{"cmd": "-- Exercice 1 : r\u00e9union de trois ouverts.\n-- TODO etudiant : remplacez sorry par la preuve (une application de IsOpen.union \u00e0 deux reprises).\nvariable {X : Type*} [TopologicalSpace X] {s t u : Set X}\n\nexample (hs : IsOpen s) (ht : IsOpen t) (hu : IsOpen u) : IsOpen (s \u222a t \u222a u) := by\n  sorry", "env": 5}

Raw output

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 6, "column": 2},
   "goal":
   "X✝⁴ : Type u_1\ninst✝⁶ : TopologicalSpace X✝⁴\ns✝¹ t✝ : Set X✝⁴\nX✝³ : Type u_2\ninst✝⁵ : TopologicalSpace X✝³\ns✝ : Set X✝³\nx : X✝³\nX✝² : Type u_3\nY : Type u_4\ninst✝⁴ : TopologicalSpace X✝²\ninst✝³ : TopologicalSpace Y\nf : X✝² → Y\nX✝¹ : Type u_5\ninst✝² : TopologicalSpace X✝¹\nX✝ : Type u_6\ninst✝¹ : TopologicalSpace X✝\nX : Type u_7\ninst✝ : TopologicalSpace X\ns t u : Set X\nhs : IsOpen s\nht : IsOpen t\nhu : IsOpen u\n⊢ IsOpen (s ∪ t ∪ u)",
   "endPos": {"line": 6, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 6}

Exercice 2 — L’image réciproque par une composée

Munkres §18, théorème 7 : une composée de continues est continue. Prouvez-le directement depuis la définition continuous_def — sans invoquer Continuous.comp (qui est exactement ce théorème, et donnerait la solution en une ligne : cherchez-le après avoir essayé).

-- Exercice 2 : la composée de deux applications continues est continue.
-- TODO etudiant : remplacez sorry par la preuve via continuous_def (indice : (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s),
-- et Set.preimage_comp le réécrit).
variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
  {f : X → Y} {g : Y → Z}

example (hf : Continuous f) (hg : Continuous g) : Continuous (g ∘ f) := by
  sorry

-- Exercice 2 : la composée de deux applications continues est continue.

-- TODO etudiant : remplacez sorry par la preuve via continuous_def (indice : (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s),

-- et Set.preimage_comp le réécrit).

variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

  {f : X → Y} {g : Y → Z}

example (hf : Continuous f) (hg : Continuous g) : Continuous (g ∘ f) := by🟨 declaration uses `sorry`

  sorry

--% env 7

--% prove 1

Raw input

{"cmd": "-- Exercice 2 : la compos\u00e9e de deux applications continues est continue.\n-- TODO etudiant : remplacez sorry par la preuve via continuous_def (indice : (g \u2218 f) \u207b\u00b9' s = f \u207b\u00b9' (g \u207b\u00b9' s),\n-- et Set.preimage_comp le r\u00e9\u00e9crit).\nvariable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]\n  {f : X \u2192 Y} {g : Y \u2192 Z}\n\nexample (hf : Continuous f) (hg : Continuous g) : Continuous (g \u2218 f) := by\n  sorry", "env": 6}

Raw output

{"sorries":
 [{"proofState": 1,
   "pos": {"line": 8, "column": 2},
   "goal":
   "X✝⁵ : Type u_1\ninst✝⁹ : TopologicalSpace X✝⁵\ns✝¹ t✝ : Set X✝⁵\nX✝⁴ : Type u_2\ninst✝⁸ : TopologicalSpace X✝⁴\ns✝ : Set X✝⁴\nx : X✝⁴\nX✝³ : Type u_3\nY✝ : Type u_4\ninst✝⁷ : TopologicalSpace X✝³\ninst✝⁶ : TopologicalSpace Y✝\nf✝ : X✝³ → Y✝\nX✝² : Type u_5\ninst✝⁵ : TopologicalSpace X✝²\nX✝¹ : Type u_6\ninst✝⁴ : TopologicalSpace X✝¹\nX✝ : Type u_7\ninst✝³ : TopologicalSpace X✝\ns t u : Set X✝\nX : Type u_8\nY : Type u_9\nZ : Type u_10\ninst✝² : TopologicalSpace X\ninst✝¹ : TopologicalSpace Y\ninst✝ : TopologicalSpace Z\nf : X → Y\ng : Y → Z\nhf : Continuous f\nhg : Continuous g\n⊢ Continuous (g ∘ f)",
   "endPos": {"line": 8, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 7}

Exercice 3 — Le complémentaire d’un ouvert

La dualité ouvert/fermé du §17 : montrer que si \(s\) est ouvert, alors \(s^\complement\) est… la bonne notion à trouver. Puis en déduire l’identité closure s = (interior sᶜ)ᶜ — c’est la composition des deux dualités prouvées en section 2.

-- Exercice 3 : la double dualité adhérence/intérieur.
-- TODO etudiant : remplacez sorry. Indice : partez de interior_compl s (prouvé en section 2)
-- et prenez le complémentaire des deux côtés, ou appliquez interior_compl au bon ensemble.
variable {X : Type*} [TopologicalSpace X] {s : Set X}

example : closure s = (interior sᶜ)ᶜ := by
  sorry

-- Exercice 3 : la double dualité adhérence/intérieur.

-- TODO etudiant : remplacez sorry. Indice : partez de interior_compl s (prouvé en section 2)

-- et prenez le complémentaire des deux côtés, ou appliquez interior_compl au bon ensemble.

variable {X : Type*} [TopologicalSpace X] {s : Set X}

example : closure s = (interior sᶜ)ᶜ := by🟨 declaration uses `sorry`

  sorry

--% env 8

--% prove 2

Raw input

{"cmd": "-- Exercice 3 : la double dualit\u00e9 adh\u00e9rence/int\u00e9rieur.\n-- TODO etudiant : remplacez sorry. Indice : partez de interior_compl s (prouv\u00e9 en section 2)\n-- et prenez le compl\u00e9mentaire des deux c\u00f4t\u00e9s, ou appliquez interior_compl au bon ensemble.\nvariable {X : Type*} [TopologicalSpace X] {s : Set X}\n\nexample : closure s = (interior s\u1d9c)\u1d9c := by\n  sorry", "env": 7}

Raw output

{"sorries":
 [{"proofState": 2,
   "pos": {"line": 7, "column": 2},
   "goal":
   "X✝⁶ : Type u_1\ninst✝¹⁰ : TopologicalSpace X✝⁶\ns✝² t✝ : Set X✝⁶\nX✝⁵ : Type u_2\ninst✝⁹ : TopologicalSpace X✝⁵\ns✝¹ : Set X✝⁵\nx : X✝⁵\nX✝⁴ : Type u_3\nY✝ : Type u_4\ninst✝⁸ : TopologicalSpace X✝⁴\ninst✝⁷ : TopologicalSpace Y✝\nf✝ : X✝⁴ → Y✝\nX✝³ : Type u_5\ninst✝⁶ : TopologicalSpace X✝³\nX✝² : Type u_6\ninst✝⁵ : TopologicalSpace X✝²\nX✝¹ : Type u_7\ninst✝⁴ : TopologicalSpace X✝¹\ns✝ t u : Set X✝¹\nX✝ : Type u_8\nY : Type u_9\nZ : Type u_10\ninst✝³ : TopologicalSpace X✝\ninst✝² : TopologicalSpace Y\ninst✝¹ : TopologicalSpace Z\nf : X✝ → Y\ng : Y → Z\nX : Type u_11\ninst✝ : TopologicalSpace X\ns : Set X\n⊢ closure s = (interior sᶜ)ᶜ",
   "endPos": {"line": 7, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 8}

8. Pour aller plus loin

Le manuel : James R. Munkres, Topology (2e éd., Prentice Hall, 2000) — les sections citées dans ce notebook (§12-§13, §17-§19, §18, §26-§27, §23-§25) en sont les chapitres 2 à 4.
Mathlib : la documentation de Mathlib.Topology pour suivre l’organisation des modules ; le fichier Mathlib/Topology/Basic.lean lui-même est une lecture remarquablement proche du manuel.
Les deux autres visages de Munkres : le volet 1/3 de cette série hommage — l’algorithme de Kuhn-Munkres pour l’affectation (issue #12598, lake assignment_lean) — et le volet 2/3, le musicien (voice leading par affectation, issue #12599).
Terry Tao et la théorie analytique des nombres (Lean-6 §6.1) : l’autre encart culturel « mathématicien dans Mathlib » de la série, pour comparer les styles d’hommage.

Série hommage James R. Munkres (1930-2026) : 1/3 l’algoriste · 2/3 le musicien · 3/3 le topologue (ce notebook). Sources : MIT Mathematics (2026-08-13), obituaires Boston Globe/Legacy et Douglass Funeral Home (Bedford, MA).

Retour au sommet