Theorems · Theorem · functional analysis

ContinuousLinearMap.isCompact_closure_image_coe_of_bounded

∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] [ProperSpace F]
  {s : Set (E' →SL[σ₁₂] F)}, Bornology.IsBounded s → IsCompact (closure (DFunLike.coe '' s))

Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values in a proper space. Then s interpreted as a set in the space of maps E → F with topology of pointwise convergence is precompact: its closure is a compact set.

Defined in

Mathlib.Analysis.Normed.Operator.Completeness

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNontriviallyNormedFieldNontriviallyNormedFieldNormedSpaceSeminormedAddCommGroupNormedSpaceRingHomIsometricProperSpace