[GOAL]
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_3
M₂ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ IsCompactOperator f ↔ ∃ V, V ∈ 𝓝 0 ∧ IsCompact (closure (f '' V))
[PROOFSTEP]
rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_3
M₂ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ (∃ V, V ∈ 𝓝 0 ∧ ∃ K, IsCompact K ∧ f '' V ⊆ K) ↔ ∃ V, V ∈ 𝓝 0 ∧ IsCompact (closure (f '' V))
[PROOFSTEP]
exact
  ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, isCompact_closure_of_subset_compact hK hKV⟩, fun ⟨V, hV, hVc⟩ =>
    ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩
[GOAL]
𝕜₁ : 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
[PROOFSTEP]
rw [image_subset_iff, preimage_smul_setₛₗ _ _ _ f this.isUnit]
[GOAL]
𝕜₁ : 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
[PROOFSTEP]
exact hrS c hc.le
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜₁
inst✝⁶ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : NormedSpace 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
S : Set M₁
hS : Metric.Bounded S
⊢ IsVonNBounded 𝕜₁ S
[PROOFSTEP]
rwa [NormedSpace.isVonNBounded_iff, ← Metric.bounded_iff_isBounded]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁶ : SeminormedAddCommGroup M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : NormedSpace 𝕜₁ M₁
inst✝² : Module 𝕜₂ M₂
inst✝¹ : ContinuousConstSMul 𝕜₂ M₂
inst✝ : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
S : Set M₁
hS : Metric.Bounded S
⊢ IsVonNBounded 𝕜₁ S
[PROOFSTEP]
rwa [NormedSpace.isVonNBounded_iff, ← Metric.bounded_iff_isBounded]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : CommSemiring R₃
inst✝⁹ : CommSemiring R₄
σ₁₂ : R₁ →+* R₂
σ₁₄ : R₁ →+* R₄
σ₃₄ : R₃ →+* R₄
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommGroup M₃
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : TopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f - g)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : CommSemiring R₃
inst✝⁹ : CommSemiring R₄
σ₁₂ : R₁ →+* R₂
σ₁₄ : R₁ →+* R₄
σ₃₄ : R₃ →+* R₄
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommGroup M₃
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : TopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + -g)
[PROOFSTEP]
exact hf.add hg.neg
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
f : M₂ → M₃
hf : IsCompactOperator f
g : M₁ →SL[σ₁₂] M₂
⊢ IsCompactOperator (f ∘ ↑g)
[PROOFSTEP]
have := g.continuous.tendsto 0
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
f : M₂ → M₃
hf : IsCompactOperator f
g : M₁ →SL[σ₁₂] M₂
this : Tendsto (↑g) (𝓝 0) (𝓝 (↑g 0))
⊢ IsCompactOperator (f ∘ ↑g)
[PROOFSTEP]
rw [map_zero] at this 
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
f : M₂ → M₃
hf : IsCompactOperator f
g : M₁ →SL[σ₁₂] M₂
this : Tendsto (↑g) (𝓝 0) (𝓝 0)
⊢ IsCompactOperator (f ∘ ↑g)
[PROOFSTEP]
rcases hf with ⟨K, hK, hKf⟩
[GOAL]
case intro.intro
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
f : M₂ → M₃
g : M₁ →SL[σ₁₂] M₂
this : Tendsto (↑g) (𝓝 0) (𝓝 0)
K : Set M₃
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ IsCompactOperator (f ∘ ↑g)
[PROOFSTEP]
exact ⟨K, hK, this hKf⟩
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
hf : IsCompactOperator f
g : M₂ → M₃
hg : Continuous g
⊢ IsCompactOperator (g ∘ f)
[PROOFSTEP]
rcases hf with ⟨K, hK, hKf⟩
[GOAL]
case intro.intro
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ IsCompactOperator (g ∘ f)
[PROOFSTEP]
refine' ⟨g '' K, hK.image hg, mem_of_superset hKf _⟩
[GOAL]
case intro.intro
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ g ∘ f ⁻¹' (g '' K)
[PROOFSTEP]
rw [preimage_comp]
[GOAL]
case intro.intro
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ f ⁻¹' (g ⁻¹' (g '' K))
[PROOFSTEP]
exact preimage_mono (subset_preimage_image _ _)
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
⊢ Continuous ↑f
[PROOFSTEP]
letI : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace _
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
this : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
⊢ Continuous ↑f
[PROOFSTEP]
haveI : UniformAddGroup M₂ := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
⊢ Continuous ↑f
[PROOFSTEP]
refine' continuous_of_continuousAt_zero f fun U hU => _
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 (↑f 0)
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
rw [map_zero] at hU 
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
rcases hf with
  ⟨K, hK, hKf⟩
    -- But any compact set is totally bounded, hence Von-Neumann bounded. Thus, `K` absorbs `U`.
      -- This gives `r > 0` such that `∀ a : 𝕜₂, r ≤ ‖a‖ → K ⊆ a • U`.
[GOAL]
case intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
rcases hK.totallyBounded.isVonNBounded 𝕜₂ hU with
  ⟨r, hr, hrU⟩
    -- Choose `c : 𝕜₂` with `r < ‖c‖`.
[GOAL]
case intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
rcases NormedField.exists_lt_norm 𝕜₁ r with ⟨c, hc⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
have hcnz : c ≠ 0 := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm
[GOAL]
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
suffices (σ₁₂ <| c⁻¹) • K ⊆ U by
  refine' mem_of_superset _ this
  have : IsUnit c⁻¹ := hcnz.isUnit.inv
  rwa [mem_map, preimage_smul_setₛₗ _ _ _ f this, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]
    -- Since `σ₁₂ c⁻¹` = `(σ₁₂ c)⁻¹`, we have to prove that `K ⊆ σ₁₂ c • U`.
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝¹ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this✝ : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this : ↑σ₁₂ c⁻¹ • K ⊆ U
⊢ U ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
refine' mem_of_superset _ this
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝¹ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this✝ : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this : ↑σ₁₂ c⁻¹ • K ⊆ U
⊢ ↑σ₁₂ c⁻¹ • K ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
have : IsUnit c⁻¹ := hcnz.isUnit.inv
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝² : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this✝¹ : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this✝ : ↑σ₁₂ c⁻¹ • K ⊆ U
this : IsUnit c⁻¹
⊢ ↑σ₁₂ c⁻¹ • K ∈ map (↑f) (𝓝 0)
[PROOFSTEP]
rwa [mem_map, preimage_smul_setₛₗ _ _ _ f this, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]
  -- Since `σ₁₂ c⁻¹` = `(σ₁₂ c)⁻¹`, we have to prove that `K ⊆ σ₁₂ c • U`.
[GOAL]
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ ↑σ₁₂ c⁻¹ • K ⊆ U
[PROOFSTEP]
rw [map_inv₀, ← subset_set_smul_iff₀ ((map_ne_zero σ₁₂).mpr hcnz)]
  -- But `σ₁₂` is isometric, so `‖σ₁₂ c‖ = ‖c‖ > r`, which concludes the argument since
    -- `∀ a : 𝕜₂, r ≤ ‖a‖ → K ⊆ a • U`.
[GOAL]
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ K ⊆ ↑σ₁₂ c • U
[PROOFSTEP]
refine' hrU (σ₁₂ c) _
[GOAL]
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ ‖↑σ₁₂ c‖
[PROOFSTEP]
rw [RingHomIsometric.is_iso]
[GOAL]
case intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : TopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : TopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂
this : UniformAddGroup M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ↑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : 0 < r
hrU : ∀ (a : 𝕜₂), r ≤ ‖a‖ → K ⊆ a • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ ‖c‖
[PROOFSTEP]
exact hc.le
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
⊢ IsClosed {f | IsCompactOperator ↑f}
[PROOFSTEP]
refine' isClosed_of_closure_subset _
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
⊢ closure {f | IsCompactOperator ↑f} ⊆ {f | IsCompactOperator ↑f}
[PROOFSTEP]
rintro u hu
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : u ∈ closure {f | IsCompactOperator ↑f}
⊢ u ∈ {f | IsCompactOperator ↑f}
[PROOFSTEP]
rw [mem_closure_iff_nhds_zero] at hu 
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
⊢ u ∈ {f | IsCompactOperator ↑f}
[PROOFSTEP]
suffices TotallyBounded (u '' Metric.closedBall 0 1)
  by
  change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)
  rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]
  exact isCompact_of_totallyBounded_isClosed this.closure isClosed_closure
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
this : TotallyBounded (↑u '' closedBall 0 1)
⊢ u ∈ {f | IsCompactOperator ↑f}
[PROOFSTEP]
change IsCompactOperator (u : M₁ →ₛₗ[σ₁₂] M₂)
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
this : TotallyBounded (↑u '' closedBall 0 1)
⊢ IsCompactOperator ↑↑u
[PROOFSTEP]
rw [isCompactOperator_iff_isCompact_closure_image_closedBall (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
this : TotallyBounded (↑u '' closedBall 0 1)
⊢ IsCompact (closure (↑↑u '' closedBall 0 1))
[PROOFSTEP]
exact isCompact_of_totallyBounded_isClosed this.closure isClosed_closure
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
⊢ TotallyBounded (↑u '' closedBall 0 1)
[PROOFSTEP]
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
⊢ ∀ (U : Set M₂), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
intro U hU
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
⊢ ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
rcases exists_nhds_zero_half hU with ⟨V, hV, hVU⟩
[GOAL]
case intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
⊢ ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
let SV : Set M₁ × Set M₂ := ⟨closedBall 0 1, -V⟩
[GOAL]
case intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
⊢ ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
rcases hu {f | ∀ x ∈ SV.1, f x ∈ SV.2}
    (ContinuousLinearMap.hasBasis_nhds_zero.mem_of_mem
      ⟨NormedSpace.isVonNBounded_closedBall _ _ _, neg_mem_nhds_zero M₂ hV⟩) with
  ⟨v, hv, huv⟩
[GOAL]
case intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
⊢ ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
rcases totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp (hv.isCompact_closure_image_closedBall 1).totallyBounded V
    hV with
  ⟨T, hT, hTv⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
⊢ ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
have hTv : v '' closedBall 0 1 ⊆ _ := subset_closure.trans hTv
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv✝ : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
hTv : ↑v '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
⊢ ∃ t, Set.Finite t ∧ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ t), y +ᵥ U
[PROOFSTEP]
refine' ⟨T, hT, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv✝ : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
hTv : ↑v '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
⊢ ↑u '' closedBall 0 1 ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ U
[PROOFSTEP]
rw [image_subset_iff, preimage_iUnion₂] at hTv ⊢
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv✝ : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
hTv : closedBall 0 1 ⊆ ⋃ (i : M₂) (_ : i ∈ T), ↑v ⁻¹' (i +ᵥ V)
⊢ closedBall 0 1 ⊆ ⋃ (i : M₂) (_ : i ∈ T), ↑u ⁻¹' (i +ᵥ U)
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv✝ : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
hTv : closedBall 0 1 ⊆ ⋃ (i : M₂) (_ : i ∈ T), ↑v ⁻¹' (i +ᵥ V)
x : M₁
hx : x ∈ closedBall 0 1
⊢ x ∈ ⋃ (i : M₂) (_ : i ∈ T), ↑u ⁻¹' (i +ᵥ U)
[PROOFSTEP]
specialize hTv hx
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv✝ : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
hTv : x ∈ ⋃ (i : M₂) (_ : i ∈ T), ↑v ⁻¹' (i +ᵥ V)
⊢ x ∈ ⋃ (i : M₂) (_ : i ∈ T), ↑u ⁻¹' (i +ᵥ U)
[PROOFSTEP]
rw [mem_iUnion₂] at hTv ⊢
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv✝ : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
hTv : ∃ i j, x ∈ ↑v ⁻¹' (i +ᵥ V)
⊢ ∃ i j, x ∈ ↑u ⁻¹' (i +ᵥ U)
[PROOFSTEP]
rcases hTv with ⟨t, ht, htx⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : x ∈ ↑v ⁻¹' (t +ᵥ V)
⊢ ∃ i j, x ∈ ↑u ⁻¹' (i +ᵥ U)
[PROOFSTEP]
refine' ⟨t, ht, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : x ∈ ↑v ⁻¹' (t +ᵥ V)
⊢ x ∈ ↑u ⁻¹' (t +ᵥ U)
[PROOFSTEP]
rw [mem_preimage, mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, neg_add_eq_sub] at htx ⊢
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : ↑v x - t ∈ V
⊢ ↑u x - t ∈ U
[PROOFSTEP]
convert hVU _ htx _ (huv x hx) using 1
[GOAL]
case h.e'_4
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : ↑v x - t ∈ V
⊢ ↑u x - t = ↑v x - t + -↑(v - u) x
[PROOFSTEP]
rw [ContinuousLinearMap.sub_apply]
[GOAL]
case h.e'_4
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : ↑v x - t ∈ V
⊢ ↑u x - t = ↑v x - t + -(↑v x - ↑u x)
[PROOFSTEP]
abel
[GOAL]
case h.e'_4
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : UniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu✝ : u ∈ closure {f | IsCompactOperator ↑f}
hu : ∀ (U : Set (M₁ →SL[σ₁₂] M₂)), U ∈ 𝓝 0 → ∃ y, y ∈ {f | IsCompactOperator ↑f} ∧ y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ (v : M₂), v ∈ V → ∀ (w : M₂), w ∈ V → v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ↑f}
huv : v - u ∈ {f | ∀ (x : M₁), x ∈ SV.fst → ↑f x ∈ SV.snd}
T : Set M₂
hT : Set.Finite T
hTv : closure (↑↑v '' closedBall 0 1) ⊆ ⋃ (y : M₂) (_ : y ∈ T), y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : ↑v x - t ∈ V
⊢ ↑u x - t = ↑v x - t + -(↑v x - ↑u x)
[PROOFSTEP]
abel
