English
If a linear map g satisfies that for every sequence u_n → x, g(u_n) → y implies y = g(x), then g is continuous.
Русский
Если линейное отображение g обладает свойством последовательного замыкания графа: для любой последовательности u_n → x верно, что g(u_n) → y тогда y = g(x), то g непрерывно.
LaTeX
$$$\forall (hg)\, (\forall u:\mathbb{N}\to E)(x:\,E)(y:\,F),\; \text{Tendsto } u\;\text{atTop }(\mathcal{N} x) \land \text{Tendsto } (g\circ u)\;\text{atTop }(\mathcal{N} y) \Rightarrow y=gx \;\Rightarrow \text{Continuous}(g)$$$
Lean4
/-- A useful form of the **closed graph theorem** : let `f` be a linear map between two Banach
spaces. To show that `f` is continuous, it suffices to show that for any convergent sequence
`uₙ ⟶ x`, if `f(uₙ) ⟶ y` then `y = f(x)`. -/
theorem continuous_of_seq_closed_graph
(hg : ∀ (u : ℕ → E) (x y), Tendsto u atTop (𝓝 x) → Tendsto (g ∘ u) atTop (𝓝 y) → y = g x) : Continuous g :=
by
refine g.continuous_of_isClosed_graph (IsSeqClosed.isClosed ?_)
rintro φ ⟨x, y⟩ hφg hφ
refine hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) ?_
have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
ext n
exact (hφg n).symm
rw [this]
exact (continuous_snd.tendsto _).comp hφ
