coe_ofSeqClosedGraph — Mathlib

English

If a linear map g has closed graph under sequential convergence, then g is continuous.

Русский

Если линейное отображение g имеет замкнутый граф относительно последовательного предела, то g непрерывно.

LaTeX

$$$\text{coercion}$$$

Lean4

theorem coe_ofSeqClosedGraph (hg : ∀ (u : ℕ → E) (x y), Tendsto u atTop (𝓝 x) → Tendsto (g ∘ u) atTop (𝓝 y) → y = g x) :
    ↑(ContinuousLinearMap.ofSeqClosedGraph hg) = g := by
  ext
  rfl

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