𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrS : ∀ (a : 𝕜₁), r ≤ ‖a‖ → S ⊆ a • ↑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ S ⊆ c • ↑f ⁻¹' K
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrS : ∀ (a : 𝕜₁), r ≤ ‖a‖ → S ⊆ a • ↑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ ↑f '' S ⊆ ↑σ₁₂ c • K
rw [image_subset_iff, preimage_smul_setₛₗ _ _ _ f this.isUnit]
no goals
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrS : ∀ (a : 𝕜₁), r ≤ ‖a‖ → S ⊆ a • ↑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ S ⊆ c • ↑f ⁻¹' K
exact hrS c hc.le