coe_ofIsClosedGraph — Mathlib

English

Upgrade a linear map using a sequential closed-graph condition to a continuous linear map.

Русский

Улучшение линейного отображения через последовательную версию условия замкнутого графика даёт непрерывное линейное отображение.

LaTeX

$$$\text{ofSeqClosedGraph}(hg) : E \to_L[𝕜] F$ with cont := g.continuous_of_seq_closed_graph hg$$$

Lean4

theorem coe_ofIsClosedGraph (hg : IsClosed (g.graph : Set <| E × F)) : ↑(ContinuousLinearMap.ofIsClosedGraph hg) = g :=
  by
  ext
  rfl

Похожие утверждения