Theorems · Theorem · operator theory

ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E),
  IsClosed ↑A →
    ∀ [A.CoFG],
      Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔
        Topology.IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed ↑(↑(u.domRestrict A)).range

Let u : E → F be a continuous linear map, and A a closed subspace of E of finite codimension. Then u is strict with closed range if and only if its restriction u.domRestrict A : A → F is strict with closed range. This is [N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1, Prop. 1][bourbaki2023].

Defined in

Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Cited by

2 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldCompleteSpaceAddCommGroupModuleAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulTopologicalSpaceIsTopologicalAddGroupContinuousSMulSubmodule.CoFG