Cantor's intersection theorem

Proved

FamousTheorems.nonempty_sinter_of_directed_nonempty_iscompact_isclosed

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathlibtopology

Cantor's intersection theorem. A directed family of nonempty compact closed sets has nonempty intersection. In particular a nested decreasing sequence of nonempty compacts cannot shrink to nothing. Compactness is what forbids the mass escaping — for merely closed sets the conclusion fails, as $[n,\infty)$ shows, and for merely bounded sets $(0,1/n)$ shows it too. The theorem is the topological content behind the nested interval property, the construction of the Cantor set, and the standard compactness proof that a continuous function on a compact set is bounded. Formalization note. The family is directed under inclusion and each member is compact and closed. The result is Mathlib's IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25

open Filter Set Topology DirectSum

theorem nonempty_sinter_of_directed_nonempty_iscompact_isclosed :
    ∀ {X : Type u_1} [inst : TopologicalSpace X] 
    {S : Set (Set X)} [hS : Nonempty ↑S], 
    DirectedOn (fun x1 x2 => x1 ⊇ x2) S → 
    (∀ U ∈ S, U.Nonempty) → (∀ U ∈ S, IsCompact U) → (∀ U ∈ S, IsClosed U) → (⋂₀ S).Nonempty := by sorry

end FamousTheorems

Source

Listed in Mathlib's curated theorem manifests; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph