image_subset_compact_of_isVonNBounded

English

If f is a compact operator and S is Von Neumann bounded in M1, then there exists a compact set K in M2 such that f[S] ⊆ K.

Русский

Если f компактный оператор и S — Von Нейманово ограниченное множество в M1, то существует компактное множество K в M2 такое, что f[S] ⊆ K.

LaTeX

$$$\exists K\subseteq M_2, \ IsCompact(K) \land f''S \subseteq K$$$

Lean4

theorem image_subset_compact_of_isVonNBounded {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) {S : Set M₁}
    (hS : IsVonNBounded 𝕜₁ S) : ∃ K : Set M₂, IsCompact K ∧ f '' S ⊆ K :=
  let ⟨K, hK, hKf⟩ := hf
  let ⟨r, hr, hrS⟩ := (hS hKf).exists_pos
  let ⟨c, hc⟩ := NormedField.exists_lt_norm 𝕜₁ r
  let this := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm
  ⟨σ₁₂ c • K, hK.image <| continuous_id.const_smul (σ₁₂ c), by
    rw [image_subset_iff, this.isUnit.preimage_smul_setₛₗ σ₁₂]; exact hrS c hc.le⟩

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