Cor. 3.0.3 — separately continuous bilinear maps on Fréchet spaces are continuous

Proved

GarrettFA.continuous_of_separately_continuous

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

functional-analysistopological-vector-spaces

Let $X, Y, Z$ be Fréchet spaces over $\mathbb K=\mathbb R$ or $\mathbb C$ and let $\beta: X\times Y\to Z$ be a bilinear map that is continuous in each variable separately. Then

\beta : X\times Y\to Z \ \text{ is jointly continuous.}

Formalization Note $\beta$ is a $\mathbb K$ -bilinear map, given as a linear map $X\to(Y\to_{\mathbb K} Z)$ .

Preamble

import Definitions.Def_GarrettFA_IsFrechetSpace

Formal statement

namespace GarrettFA
theorem continuous_of_separately_continuous {𝕜 : Type*} [RCLike 𝕜] {X : Type*} [AddCommGroup X] [Module 𝕜 X] [Module ℝ X]
    [IsScalarTower ℝ 𝕜 X] [UniformSpace X] [IsUniformAddGroup X] [ContinuousSMul 𝕜 X] [T2Space X]
    {Y : Type*} [AddCommGroup Y] [Module 𝕜 Y] [Module ℝ Y]
    [IsScalarTower ℝ 𝕜 Y] [UniformSpace Y] [IsUniformAddGroup Y] [ContinuousSMul 𝕜 Y] [T2Space Y]
    {Z : Type*} [AddCommGroup Z] [Module 𝕜 Z] [Module ℝ Z]
    [IsScalarTower ℝ 𝕜 Z] [UniformSpace Z] [IsUniformAddGroup Z] [ContinuousSMul 𝕜 Z] [T2Space Z]
    (hX : IsFrechetSpace 𝕜 X) (hY : IsFrechetSpace 𝕜 Y) (hZ : IsFrechetSpace 𝕜 Z)
    (β : X →ₗ[𝕜] Y →ₗ[𝕜] Z) (h₁ : ∀ x : X, Continuous (β x))
    (h₂ : ∀ y : Y, Continuous (fun x : X => β x y)) :
    Continuous (fun p : X × Y => β p.1 p.2) := by sorry
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. 5, Corollary 3.0.3

Read-back

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

Let $\mathbb K$ be a real-or-complex scalar field (in practice $\mathbb R$ or $\mathbb C$ ). Let $X$ , $Y$ , $Z$ be three spaces, each of which is a $\mathbb K$ -vector space that is also a real vector space with compatible scalar multiplications, carrying a uniform structure for which addition and subtraction are uniformly continuous (the canonical translation-invariant uniformity), with jointly continuous scalar multiplication by $\mathbb K$ , and Hausdorff. Assume each of $X$ , $Y$ , $Z$ is Fréchet. Fréchet (the bundle's definition, applied to the given uniform structure): locally convex as a real topological vector space, the topology is metrizable, and the space is complete for its uniform structure (every Cauchy filter converges).

Let $\beta$ be a $\mathbb K$ -bilinear map $X\times Y\to Z$ (given as a $\mathbb K$ -linear map from $X$ to the $\mathbb K$ -linear maps $Y\to Z$ ), such that (1) for each fixed $x\in X$ the map $y\mapsto\beta(x,y)$ is continuous, and (2) for each fixed $y\in Y$ the map $x\mapsto\beta(x,y)$ is continuous. Then the map $X\times Y\to Z$ , $(x,y)\mapsto\beta(x,y)$ , is continuous for the product topology on $X\times Y$ .

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