coeFn_ofIsClosedGraph — Mathlib

English

The coercion of the upgraded map equals the original linear map.

Русский

Переход от обновленного отображения к исходной линейной карте сохраняется: коeф. равен исходной линейной карте.

LaTeX

$$$\uparrow(\text{ContinuousLinearMap.ofIsClosedGraph } hg) = g$$$

Lean4

@[simp]
theorem coeFn_ofIsClosedGraph (hg : IsClosed (g.graph : Set <| E × F)) :
    ⇑(ContinuousLinearMap.ofIsClosedGraph hg) = g :=
  rfl

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