ofIsClosedGraph — Mathlib

English

Given a linear map g and a closed graph, one can construct a continuous linear map with the same underlying linear map g.

Русский

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

LaTeX

$$$\text{ofIsClosedGraph}(hg) : E \to_L[𝕜] F$ with toLinearMap = g \text{ and } cont = g.continuous_of_isClosed_graph hg$$$

Lean4

/-- Upgrade a `LinearMap` to a `ContinuousLinearMap` using the **closed graph theorem**. -/
def ofIsClosedGraph (hg : IsClosed (g.graph : Set <| E × F)) : E →L[𝕜] F
    where
  toLinearMap := g
  cont := g.continuous_of_isClosed_graph hg

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