Fréchet space

Definition

GarrettFA_IsFrechetSpace

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysistopological-vector-spaces

A topological vector space $X$ over $\mathbb K=\mathbb R$ or $\mathbb C$ is a Fréchet space if it is

locally convex,
metrizable, and
complete for its canonical uniform structure.

Banach and Hilbert spaces are Fréchet spaces.

Formalization Note Local convexity is real local convexity. Completeness refers to the uniform structure on $X$ , which the theorems using this predicate require to be the canonical translation-invariant uniformity.

Definition code

import Mathlib

namespace GarrettFA

/-- A Fréchet space: a locally convex topological vector space whose topology is metrizable
and which is complete (for its uniform structure, which in applications is the canonical
uniformity of the topological vector space). -/
def IsFrechetSpace (𝕜 : Type*) (X : Type*) [RCLike 𝕜] [AddCommGroup X] [Module 𝕜 X]
    [Module ℝ X] [IsScalarTower ℝ 𝕜 X] [UniformSpace X] : Prop :=
  LocallyConvexSpace ℝ X ∧ TopologicalSpace.MetrizableSpace X ∧ CompleteSpace X

end GarrettFA

Source

Paul Garrett, *Completeness and quasi-completeness* (lecture notes, April 24, 2014), http://www.math.umn.edu/~garrett/m/fun/notes_2012-13/07d_quasi-completeness.pdf, p. 1 and §1.3 (Fréchet spaces as locally convex, metrizable, complete spaces)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Defines a property of a type $X$ given a real-or-complex scalar field $\mathbb K$ (in practice $\mathbb R$ or $\mathbb C$ ), a $\mathbb K$ -vector space structure on $X$ , a real vector space structure on $X$ compatible with it, and a uniform structure on $X$ . $X$ is called Fréchet when the conjunction of three conditions holds:

$X$ is locally convex as a real topological vector space (0 has a neighbourhood basis of convex sets, in the topology induced by the uniformity);
the topology induced by the uniformity is metrizable;
$X$ is complete for the given uniform structure (every Cauchy filter converges).

The definition does not by itself require that the operations are continuous or that the uniformity is the translation-invariant uniformity of a topological group; statements using it add those assumptions separately.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph