Banach open mapping theorem #

This file contains the Banach open mapping theorem, i.e., the fact that a bijective bounded linear map between Banach spaces has a bounded inverse.

source

structure ContinuousLinearMap.NonlinearRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) :

Type (max u_2 u_3)

toFun : F → E
nnnorm : NNReal
bound' : ∀ (y : F), ‖ContinuousLinearMap.NonlinearRightInverse.toFun s y‖ ≤ ↑s.nnnorm * ‖y‖
right_inv' : ∀ (y : F), ↑f (ContinuousLinearMap.NonlinearRightInverse.toFun s y) = y

A (possibly nonlinear) right inverse to a continuous linear map, which doesn't have to be linear itself but which satisfies a bound ‖inverse x‖ ≤ C * ‖x‖. A surjective continuous linear map doesn't always have a continuous linear right inverse, but it always has a nonlinear inverse in this sense, by Banach's open mapping theorem.

Instances For

source

instance ContinuousLinearMap.instCoeFunNonlinearRightInverseForAll {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) :

CoeFun (ContinuousLinearMap.NonlinearRightInverse f) fun x => F → E

Equations

ContinuousLinearMap.instCoeFunNonlinearRightInverseForAll f = { coe := fun fsymm => fsymm.toFun }

source

@[simp]

theorem ContinuousLinearMap.NonlinearRightInverse.right_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →L[𝕜] F} (fsymm : ContinuousLinearMap.NonlinearRightInverse f) (y : F) :

↑f (ContinuousLinearMap.NonlinearRightInverse.toFun fsymm y) = y

source

theorem ContinuousLinearMap.NonlinearRightInverse.bound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →L[𝕜] F} (fsymm : ContinuousLinearMap.NonlinearRightInverse f) (y : F) :

‖ContinuousLinearMap.NonlinearRightInverse.toFun fsymm y‖ ≤ ↑fsymm.nnnorm * ‖y‖

source

noncomputable def ContinuousLinearEquiv.toNonlinearRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) :

ContinuousLinearMap.NonlinearRightInverse ↑f

Given a continuous linear equivalence, the inverse is in particular an instance of ContinuousLinearMap.NonlinearRightInverse (which turns out to be linear).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable instance instInhabitedNonlinearRightInverseToContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldIdToNonAssocSemiringIdsToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToModule {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃L[𝕜] F) :

Inhabited (ContinuousLinearMap.NonlinearRightInverse ↑f)

Equations

One or more equations did not get rendered due to their size.

Proof of the Banach open mapping theorem #

source

theorem ContinuousLinearMap.exists_approx_preimage_norm_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] (surj : Function.Surjective ↑f) :

∃ C, C ≥ 0 ∧ ∀ (y : F), ∃ x, dist (↑f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖

First step of the proof of the Banach open mapping theorem (using completeness of F): by Baire's theorem, there exists a ball in E whose image closure has nonempty interior. Rescaling everything, it follows that any y ∈ F is arbitrarily well approached by images of elements of norm at most C * ‖y‖. For further use, we will only need such an element whose image is within distance ‖y‖/2 of y, to apply an iterative process.

source

theorem ContinuousLinearMap.exists_preimage_norm_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ↑f) :

∃ C, C > 0 ∧ ∀ (y : F), ∃ x, ↑f x = y ∧ ‖x‖ ≤ C * ‖y‖

The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then any point has a preimage with controlled norm.

source

theorem ContinuousLinearMap.isOpenMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ↑f) :

IsOpenMap ↑f

The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is open.

source

theorem ContinuousLinearMap.quotientMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ↑f) :

QuotientMap ↑f

source

theorem AffineMap.isOpenMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {P : Type u_4} {Q : Type u_5} [MetricSpace P] [NormedAddTorsor E P] [MetricSpace Q] [NormedAddTorsor F Q] (f : P →ᵃ[𝕜] Q) (hf : Continuous ↑f) (surj : Function.Surjective ↑f) :

IsOpenMap ↑f

Applications of the Banach open mapping theorem #

source

theorem ContinuousLinearMap.interior_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ↑f) (s : Set F) :

interior (↑f ⁻¹' s) = ↑f ⁻¹' interior s

source

theorem ContinuousLinearMap.closure_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ↑f) (s : Set F) :

closure (↑f ⁻¹' s) = ↑f ⁻¹' closure s

source

theorem ContinuousLinearMap.frontier_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ↑f) (s : Set F) :

frontier (↑f ⁻¹' s) = ↑f ⁻¹' frontier s

source

theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hsurj : LinearMap.range f = ⊤) :

∃ fsymm, 0 < fsymm.nnnorm

source

theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_def {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hsurj : LinearMap.range f = ⊤) :

ContinuousLinearMap.nonlinearRightInverseOfSurjective f hsurj = Classical.choose (_ : ∃ fsymm, 0 < fsymm.nnnorm)

source

@[irreducible]

noncomputable def ContinuousLinearMap.nonlinearRightInverseOfSurjective {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hsurj : LinearMap.range f = ⊤) :

ContinuousLinearMap.NonlinearRightInverse f

A surjective continuous linear map between Banach spaces admits a (possibly nonlinear) controlled right inverse. In general, it is not possible to ensure that such a right inverse is linear (take for instance the map from E to E/F where F is a closed subspace of E without a closed complement. Then it doesn't have a continuous linear right inverse.)

Equations

@ContinuousLinearMap.nonlinearRightInverseOfSurjective = ContinuousLinearMap.wrapped✝.1

Instances For

source

theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hsurj : LinearMap.range f = ⊤) :

0 < (ContinuousLinearMap.nonlinearRightInverseOfSurjective f hsurj).nnnorm

source

theorem LinearEquiv.continuous_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[𝕜] F) (h : Continuous ↑e) :

Continuous ↑(LinearEquiv.symm e)

If a bounded linear map is a bijection, then its inverse is also a bounded linear map.

source

def LinearEquiv.toContinuousLinearEquivOfContinuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[𝕜] F) (h : Continuous ↑e) :

E ≃L[𝕜] F

Associating to a linear equivalence between Banach spaces a continuous linear equivalence when the direct map is continuous, thanks to the Banach open mapping theorem that ensures that the inverse map is also continuous.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[𝕜] F) (h : Continuous ↑e) :

↑(LinearEquiv.toContinuousLinearEquivOfContinuous e h) = ↑e

source

@[simp]

theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (e : E ≃ₗ[𝕜] F) (h : Continuous ↑e) :

↑(ContinuousLinearEquiv.symm (LinearEquiv.toContinuousLinearEquivOfContinuous e h)) = ↑(LinearEquiv.symm e)

source

noncomputable def ContinuousLinearEquiv.ofBijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) :

E ≃L[𝕜] F

Convert a bijective continuous linear map f : E →L[𝕜] F from a Banach space to a normed space to a continuous linear equivalence.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem ContinuousLinearEquiv.coeFn_ofBijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) :

↑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = ↑f

source

theorem ContinuousLinearEquiv.coe_ofBijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) :

↑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = f

source

@[simp]

theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) (x : E) :

↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.ofBijective f hinj hsurj)) (↑f x) = x

source

@[simp]

theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) (y : F) :

↑f (↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.ofBijective f hinj hsurj)) y) = y

source

noncomputable def ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace { x // x ∈ G }] (hker : LinearMap.ker f = ⊥) :

(E × { x // x ∈ G }) ≃L[𝕜] F

Intermediate definition used to show ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot.

This is f.coprod G.subtypeL as a ContinuousLinearEquiv.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace { x // x ∈ G }] (hker : LinearMap.ker f = ⊥) :

LinearMap.range f = Submodule.map (↑↑(ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl f h hker)) (Submodule.prod ⊤ ⊥)

source

theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (f : E →L[𝕜] F) (G : Submodule 𝕜 F) (h : IsCompl (LinearMap.range f) G) (hG : IsClosed ↑G) (hker : LinearMap.ker f = ⊥) :

IsClosed ↑(LinearMap.range f)

source

theorem LinearMap.continuous_of_isClosed_graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (g : E →ₗ[𝕜] F) (hg : IsClosed ↑(LinearMap.graph g)) :

Continuous ↑g

The closed graph theorem : a linear map between two Banach spaces whose graph is closed is continuous.

source

theorem LinearMap.continuous_of_seq_closed_graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] (g : E →ₗ[𝕜] F) (hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (↑g ∘ u) Filter.atTop (nhds y) → y = ↑g x) :

Continuous ↑g

A useful form of the closed graph theorem : let f be a linear map between two Banach spaces. To show that f is continuous, it suffices to show that for any convergent sequence uₙ ⟶ x, if f(uₙ) ⟶ y then y = f(x).

source

def ContinuousLinearMap.ofIsClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑(LinearMap.graph g)) :

E →L[𝕜] F

Upgrade a LinearMap to a ContinuousLinearMap using the closed graph theorem.

Equations

ContinuousLinearMap.ofIsClosedGraph hg = ContinuousLinearMap.mk g

Instances For

source

@[simp]

theorem ContinuousLinearMap.coeFn_ofIsClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑(LinearMap.graph g)) :

↑(ContinuousLinearMap.ofIsClosedGraph hg) = ↑g

source

theorem ContinuousLinearMap.coe_ofIsClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑(LinearMap.graph g)) :

↑(ContinuousLinearMap.ofIsClosedGraph hg) = g

source

def ContinuousLinearMap.ofSeqClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {g : E →ₗ[𝕜] F} (hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (↑g ∘ u) Filter.atTop (nhds y) → y = ↑g x) :

E →L[𝕜] F

Upgrade a LinearMap to a ContinuousLinearMap using a variation on the closed graph theorem.

Equations

ContinuousLinearMap.ofSeqClosedGraph hg = ContinuousLinearMap.mk g

Instances For

source

@[simp]

theorem ContinuousLinearMap.coeFn_ofSeqClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {g : E →ₗ[𝕜] F} (hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (↑g ∘ u) Filter.atTop (nhds y) → y = ↑g x) :

↑(ContinuousLinearMap.ofSeqClosedGraph hg) = ↑g

source

theorem ContinuousLinearMap.coe_ofSeqClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [CompleteSpace E] {g : E →ₗ[𝕜] F} (hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (↑g ∘ u) Filter.atTop (nhds y) → y = ↑g x) :

↑(ContinuousLinearMap.ofSeqClosedGraph hg) = g