TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (claude-sonnet-5 + deepseek-v4-pro)verified 2026-08-05 (claude-sonnet-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection

Statement

Let $(X, T)$ be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). For a family $A$ of subsets of $X$ write

$⋂ A : = {x \in X : x \in A for every A \in A},$

so that $⋂ \emptyset = X$ , matching the convention for the empty finite intersection in Finite intersection property. Then:

$(X, T)$ is compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) if and only if every family $A$ of closed subsets of $X$ with the finite intersection property (Finite intersection property) satisfies $⋂ A \neq \emptyset$ .
Equivalently: $(X, T)$ is compact if and only if every family of closed subsets of $X$ that is contained in some filter on $X$ (Filter on a set) has nonempty intersection, a family of subsets of $X$ lying in a filter exactly when it has the finite intersection property (A family lies in a filter exactly when it has the finite intersection property).

No choice principle is used in either direction: complementation is a canonical bijection, so no member of a family ever has to be selected.

Facts & Assumptions

Given: A topological space $(X, T)$ .

[A1]

For a family $A$ of subsets of $X$ write $A^{c} : = {X ∖ A : A \in A}$ .

[L1]

A subset $F \subseteq X$ is closed exactly when $X ∖ F \in T$ , and $X ∖ (X ∖ F) = F$ for every $F \subseteq X$ (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L2]

$(X, T)$ is compact exactly when every family $U \subseteq T$ with $⋃ U = X$ has a finite subfamily with union $X$ , a family being finite when it is empty or listable as ${V_{0}, \dots, V_{n}}$ for some $n \in N$ (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L3]

$A$ has the finite intersection property when $⋂_{i \in n} s (i) \neq \emptyset$ for every $n \in N$ and every finite list $s : n \to A$ , the intersection over $n = 0$ being $X$ (Finite intersection property).

[L4]

A family of subsets of $X$ is contained in some filter on $X$ if and only if it has the finite intersection property (A family lies in a filter exactly when it has the finite intersection property, Filter on a set).

Proof

technique · direct

1.1

The operation $A \mapsto A^{c}$ of [A1] carries families of closed subsets of $X$ to families of open subsets of $X$ and back, and satisfies $(A^{c})^{c} = A$ , so it is a bijection between the two collections.

A1L1

1.2

For every family $A$ of subsets of $X$ one has $X ∖ ⋂ A = ⋃ A^{c}$ , since a point of $X$ fails to lie in every member of $A$ exactly when it lies in the complement of some member; with $⋂ \emptyset = X$ and $⋃ \emptyset = \emptyset$ the identity also holds at $A = \emptyset$ . Hence $⋂ A = \emptyset$ if and only if $⋃ A^{c} = X$ .

A1L1L3

2.1

The same identity applied to finitely many members: for $n \in N$ and a finite list $s : n \to A$ one has $⋂_{i \in n} s (i) = \emptyset$ exactly when ${X ∖ s (i) : i \in n}$ , a finite subfamily of $A^{c}$ , has union $X$ ; and every finite subfamily of $A^{c}$ arises from such a list. So $A$ has the finite intersection property if and only if no finite subfamily of $A^{c}$ has union $X$ .

L2L3step 1.1step 1.2

3.1

Assume $(X, T)$ is compact and let $A$ be a family of closed subsets of $X$ with $⋂ A = \emptyset$ ; then $A^{c}$ is a family of open sets by step 1.1 and has union $X$ by step 1.2, so it is an open cover, compactness supplies a finite subfamily of it with union $X$ , and by step 2.1 the family $A$ fails the finite intersection property. Contraposing over $A$ : every family of closed subsets of $X$ with the finite intersection property has nonempty intersection.

L2step 1.1step 1.2step 2.1

3.2

Conversely assume every family of closed subsets of $X$ with the finite intersection property has nonempty intersection, and let $U$ be an open cover of $X$ ; then $A : = U^{c}$ is a family of closed subsets of $X$ with $A^{c} = U$ by step 1.1 and $⋂ A = \emptyset$ by step 1.2, so $A$ fails the finite intersection property, and by step 2.1 some finite subfamily of $U$ has union $X$ . So every open cover of $X$ has a finite subcover and $(X, T)$ is compact.

L2step 1.1step 1.2step 2.1

4.1

Claim 1 is proved by steps 3.1 and 3.2, and claim 2 follows from it by [L4], which replaces the phrase "has the finite intersection property" by "is contained in some filter on $X$ " without changing what is being quantified over.

L4step 3.1step 3.2∎

Remarks

What the condition says, and why it is the useful form. Compactness in the open-cover form is a statement about families that already cover; the closed-set form is a statement about families that already have all their finite intersections nonempty. In practice the second is easier to apply, because a nested family of nonempty closed sets has the finite intersection property for free, and the theorem then produces a point lying in all of them at once. That is how it is used below in Assuming dependent choice, every locally compact Hausdorff space is a Baire space, whose step 7.1 turns a decreasing sequence of nonempty closed sets into a point common to all of them. In a compact Hausdorff space every quasicomponent is connected, so quasicomponents and components coincide uses the theorem in the opposite direction: from a family of closed sets whose intersection is empty it extracts a finite subfamily whose intersection is already empty.

The finite intersection property is not a topological notion. Finite intersection property is a condition on an arbitrary family of subsets of a set, and A family lies in a filter exactly when it has the finite intersection property shows it is exactly the condition for the family to sit inside a filter. The topology enters this theorem only through the word "closed"; the theorem is that compactness of the topology is what makes that combinatorial condition detect a common point.

The metric special case is A metric space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection, stated there for a metric space and its closed sets. It is not used above, and it is not needed: by For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide the metric statement is the present one applied to a metric topology.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Finite intersection property (Wikipedia) (standard reference, not scraped)
Compact space (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §26 (standard reference, not scraped)
Stacks Project, Tag 0059 (standard reference, not scraped)