Equicontinuous set of maps

Definition

GarrettFA_IsEquicontinuousSet

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

functional-analysistopological-vector-spaces

Let $X$ and $Y$ be topological vector spaces and let $S$ be a set of maps $X\to Y$ . The set $S$ is equicontinuous if for every neighbourhood $U$ of $0$ in $Y$ there is a neighbourhood $N$ of $0$ in $X$ such that

T(N)\subseteq U\qquad\text{for every } T\in S.

For sets of linear maps this is uniform equicontinuity. It is the conclusion of the Banach–Steinhaus theorem.

Formalization Note The predicate is stated for an arbitrary set of functions; linear maps enter through their coercions to functions.

Definition code

import Mathlib

namespace GarrettFA

open Topology

/-- Garrett, *Completeness and quasi-completeness*, §2.2. A set `S` of maps `X → Y` between
topological vector spaces is equicontinuous when for every neighbourhood `U` of `0` in `Y`
there is a neighbourhood `N` of `0` in `X` with `T(N) ⊆ U` for every `T ∈ S`. -/
def IsEquicontinuousSet {X Y : Type*} [TopologicalSpace X] [Zero X] [TopologicalSpace Y] [Zero Y]
    (S : Set (X → Y)) : Prop :=
  ∀ U ∈ 𝓝 (0 : Y), ∃ N ∈ 𝓝 (0 : X), ∀ T ∈ S, Set.MapsTo T N U

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. 4, §2.2 (definition of equicontinuity)

Read-back

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

Defines a property of a set $S$ of functions $X\to Y$ , where $X$ and $Y$ are types each carrying a topology and a distinguished element $0$ (no algebraic or linearity structure is assumed, and the functions in $S$ are arbitrary functions, not necessarily linear or continuous). $S$ is called equicontinuous when for every neighbourhood $U$ of $0$ in $Y$ there is a neighbourhood $N$ of $0$ in $X$ such that $T(N)\subseteq U$ for every $T\in S$ . Only the behaviour at the point $0$ is constrained; the condition does not require $T(0)=0$ explicitly, but taking $U$ small forces $T(0)$ to lie in every neighbourhood of $0$ . The empty set $S$ satisfies the condition trivially.

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