Existing in Mathlib · Functional analysis

Banach Open Mapping Theorem

A surjective continuous semilinear map between complete normed spaces cannot crush every neighborhood into a thin set: it sends every open set to an open set.

Banach spaces
continuous semilinear maps
surjectivity
open maps
Baire category

Exact theorem

Exact Mathlib statement

protected theorem ContinuousLinearMap.isOpenMap {𝕜 𝕜' : Type*} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective f) : IsOpenMap f

The theorem at a glance

Banach Open Mapping Theorem at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

An ivory functional-analysis poster shows a surjective continuous semilinear map carrying an open neighborhood in one complete normed space onto a region containing an open neighborhood in the other. — A surjective continuous semilinear map between Banach spaces is open.

Statement structure

From hypotheses to conclusion

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

A broad source-space neighborhood passes through a surjective linear aperture and emerges as a target region visibly containing a full open ball around each mapped point. — Completeness and surjectivity prevent a continuous semilinear map from flattening open neighborhoods.

Why it matters

A mathematical landmark

The open mapping theorem is one of functional analysis's three foundational Banach-space principles. It converts algebraic surjectivity and analytic completeness into robust topological control.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's open-mapping result for a surjective continuous semilinear map between complete normed spaces over isometrically equivalent nontrivially normed fields. It concludes that the map is open. It does not assume or conclude injectivity, construct a continuous linear inverse, or state the closed graph theorem.

Surjectivity is required; injectivity is neither required nor concluded.
The selected declaration says that images of open sets are open; it does not itself package a continuous inverse.
The scalar context allows a semilinear map between isometrically equivalent nontrivially normed fields.

Source and local evidence

Where the theorem comes from

Existing declaration: ContinuousLinearMap.isOpenMap in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.banach-open-mapping-theorem.v001
Source: Open the pinned upstream reference