Topology

Heine–Borel Theorem

In ℝⁿ, a subset is compact if and only if it is closed and bounded

lean4-prooftopologycompactnessvisualization

Bolzano–Weierstrass Theorem

Every bounded sequence in ℝⁿ has a convergent subsequence

lean4-prooftopologysequencescompactnessvisualization

Brouwer Fixed-Point Theorem

Every continuous map from a compact convex set to itself has a fixed point

lean4-prooftopologyfixed-pointvisualization

Urysohn's Lemma

In a normal space, disjoint closed sets can be separated by a continuous function

lean4-prooftopologyseparationvisualization

Tychonoff's Theorem

An arbitrary product of compact spaces is compact in the product topology

lean4-prooftopologycompactnessproductvisualization

Path-Connected Implies Connected

Every path-connected topological space is connected; continuous paths prevent disconnections

lean4-prooftopologyvisualization

Connected Components

Every topological space partitions into maximal connected subsets, each of which is closed

lean4-prooftopologyvisualization

Quotient Topology

The quotient topology makes the projection continuous and is universal for maps out of the quotient

lean4-prooftopologyvisualization

Product Topology

A map into a product space is continuous iff every coordinate projection composed with it is continuous

lean4-prooftopologyvisualization

Subspace Topology

The subspace topology on a subset S of X is the coarsest topology making the inclusion map continuous

lean4-prooftopologyvisualization

Hausdorff Implies T1

Every Hausdorff (T2) space is a T1 space, meaning singletons are closed sets

lean4-prooftopologyvisualization

Continuous Image of Compact is Compact

The continuous image of a compact set is compact, a cornerstone of analysis and topology

lean4-prooftopologyvisualization

Compact Subset of Hausdorff is Closed

In a Hausdorff space every compact subset is closed, generalising the Heine–Borel direction compact implies closed

lean4-prooftopologyvisualization

Baire Category Theorem

In a complete metric space, the intersection of countably many dense open sets is dense

lean4-prooftopologyvisualization

Separable Spaces

A topological space is separable if it contains a countable dense subset

lean4-prooftopologyvisualization

Second-Countable Spaces

A topological space is second-countable if its topology has a countable basis

lean4-prooftopologyvisualization

Metrizable Spaces

A topological space is metrizable if its topology is induced by some metric

lean4-prooftopologyvisualization

Normal Space

A topological space is normal if disjoint closed sets can be separated by disjoint open neighborhoods

lean4-prooftopologyvisualization

Regular Space

A topological space is regular if a closed set and a disjoint point can be separated by open neighborhoods

lean4-prooftopologyvisualization

Alexandrov One-Point Compactification

Adding a single point at infinity to a locally compact Hausdorff space yields a compact space

lean4-prooftopologyvisualization

Continuous Bijection on Compact-Hausdorff is Homeo

A continuous bijection from a compact space to a Hausdorff space is automatically a homeomorphism

lean4-prooftopologyvisualization