English
Let g be a linear map between Banach spaces. If its graph is a closed subset of E × F, then g is continuous.
Русский
Пусть g: E → F — линейное отображение между банаховыми пространствами. Если график g в E × F замкнут, то g непрерывно.
LaTeX
$$$IsClosed(g.graph) \Rightarrow g \text{ is continuous}$$$
Lean4
/-- The **closed graph theorem** : a linear map between two Banach spaces whose graph is closed
is continuous. -/
theorem continuous_of_isClosed_graph (hg : IsClosed (g.graph : Set <| E × F)) : Continuous g :=
by
letI : CompleteSpace g.graph := completeSpace_coe_iff_isComplete.mpr hg.isComplete
let φ₀ : E →ₗ[𝕜] E × F := LinearMap.id.prod g
have : Function.LeftInverse Prod.fst φ₀ := fun x => rfl
let φ : E ≃ₗ[𝕜] g.graph := (LinearEquiv.ofLeftInverse this).trans (LinearEquiv.ofEq _ _ g.graph_eq_range_prod.symm)
let ψ : g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous continuous_subtype_val.fst
exact (continuous_subtype_val.comp ψ.symm.continuous).snd
