Theorems · Theorem · operator theory

IsCompactOperator.image_subset_compact_of_isVonNBounded

∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁]
  [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂] [inst_6 : Module 𝕜₁ M₁] [inst_7 : Module 𝕜₂ M₂]
  [ContinuousConstSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂},
  IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsVonNBounded 𝕜₁ S → ∃ K, IsCompact K ∧ ⇑f '' S ⊆ K

Defined in

Mathlib.Analysis.Normed.Operator.Compact.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedRingTopologicalSpaceAddCommMonoidTopologicalSpaceAddCommMonoidModuleModuleContinuousConstSMul