Compact operators #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define compact linear operators between two topological vector spaces (TVS).
Main definitions #
is_compact_operator: predicate for compact operators
Main statements #
is_compact_operator_iff_is_compact_closure_image_closed_ball: the usual characterization of compact operators from a normed space to a T2 TVS.is_compact_operator.comp_clm: precomposing a compact operator by a continuous linear map gives a compact operatoris_compact_operator.clm_comp: postcomposing a compact operator by a continuous linear map gives a compact operatoris_compact_operator.continuous: compact operators are automatically continuousis_closed_set_of_is_compact_operator: the set of compact operators is closed for the operator norm
Implementation details #
We define is_compact_operator as a predicate, because the space of compact operators inherits all
of its structure from the space of continuous linear maps (e.g we want to have the usual operator
norm on compact operators).
The two natural options then would be to make it a predicate over linear maps or continuous linear maps. Instead we define it as a predicate over bare functions, although it really only makes sense for linear functions, because Lean is really good at finding coercions to bare functions (whereas coercing from continuous linear maps to linear maps often needs type ascriptions).
References #
- Bourbaki, Spectral Theory, chapters 3 to 5, to be published (2022)
Tags #
Compact operator
def
is_compact_operator
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_zero M₁]
[topological_space M₁]
[topological_space M₂]
(f : M₁ → M₂) :
Prop
A compact operator between two topological vector spaces. This definition is usually given as "there exists a neighborhood of zero whose image is contained in a compact set", but we choose a definition which involves fewer existential quantifiers and replaces images with preimages.
We prove the equivalence in is_compact_operator_iff_exists_mem_nhds_image_subset_compact.
Equations
- is_compact_operator f = ∃ (K : set M₂), is_compact K ∧ f ⁻¹' K ∈ nhds 0
theorem
is_compact_operator_zero
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_zero M₁]
[topological_space M₁]
[topological_space M₂]
[has_zero M₂] :
theorem
is_compact_operator_iff_exists_mem_nhds_image_subset_compact
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₂]
(f : M₁ → M₂) :
theorem
is_compact_operator_iff_exists_mem_nhds_is_compact_closure_image
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₂]
[t2_space M₂]
(f : M₁ → M₂) :
is_compact_operator f ↔ ∃ (V : set M₁) (H : V ∈ nhds 0), is_compact (closure (f '' V))
theorem
is_compact_operator.image_subset_compact_of_vonN_bounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
{S : set M₁}
(hS : bornology.is_vonN_bounded 𝕜₁ S) :
theorem
is_compact_operator.is_compact_closure_image_of_vonN_bounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
{S : set M₁}
(hS : bornology.is_vonN_bounded 𝕜₁ S) :
is_compact (closure (⇑f '' S))
theorem
is_compact_operator.image_subset_compact_of_bounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
{S : set M₁}
(hS : metric.bounded S) :
theorem
is_compact_operator.is_compact_closure_image_of_bounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
{S : set M₁}
(hS : metric.bounded S) :
is_compact (closure (⇑f '' S))
theorem
is_compact_operator.image_ball_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
(r : ℝ) :
∃ (K : set M₂), is_compact K ∧ ⇑f '' metric.ball 0 r ⊆ K
theorem
is_compact_operator.image_closed_ball_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
(r : ℝ) :
∃ (K : set M₂), is_compact K ∧ ⇑f '' metric.closed_ball 0 r ⊆ K
theorem
is_compact_operator.is_compact_closure_image_ball
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
(r : ℝ) :
is_compact (closure (⇑f '' metric.ball 0 r))
theorem
is_compact_operator.is_compact_closure_image_closed_ball
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f)
(r : ℝ) :
is_compact (closure (⇑f '' metric.closed_ball 0 r))
theorem
is_compact_operator_iff_image_ball_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r) :
is_compact_operator ⇑f ↔ ∃ (K : set M₂), is_compact K ∧ ⇑f '' metric.ball 0 r ⊆ K
theorem
is_compact_operator_iff_image_closed_ball_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r) :
is_compact_operator ⇑f ↔ ∃ (K : set M₂), is_compact K ∧ ⇑f '' metric.closed_ball 0 r ⊆ K
theorem
is_compact_operator_iff_is_compact_closure_image_ball
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r) :
is_compact_operator ⇑f ↔ is_compact (closure (⇑f '' metric.ball 0 r))
theorem
is_compact_operator_iff_is_compact_closure_image_closed_ball
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[semi_normed_ring 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r) :
is_compact_operator ⇑f ↔ is_compact (closure (⇑f '' metric.closed_ball 0 r))
theorem
is_compact_operator.smul
{M₁ : Type u_5}
{M₂ : Type u_6}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₂]
[add_comm_monoid M₂]
{S : Type u_1}
[monoid S]
[distrib_mul_action S M₂]
[has_continuous_const_smul S M₂]
{f : M₁ → M₂}
(hf : is_compact_operator f)
(c : S) :
is_compact_operator (c • f)
theorem
is_compact_operator.add
{M₁ : Type u_5}
{M₂ : Type u_6}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₂]
[add_comm_monoid M₂]
[has_continuous_add M₂]
{f g : M₁ → M₂}
(hf : is_compact_operator f)
(hg : is_compact_operator g) :
is_compact_operator (f + g)
theorem
is_compact_operator.neg
{M₁ : Type u_5}
{M₄ : Type u_8}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₄]
[add_comm_group M₄]
[has_continuous_neg M₄]
{f : M₁ → M₄}
(hf : is_compact_operator f) :
theorem
is_compact_operator.sub
{M₁ : Type u_5}
{M₄ : Type u_8}
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₄]
[add_comm_group M₄]
[topological_add_group M₄]
{f g : M₁ → M₄}
(hf : is_compact_operator f)
(hg : is_compact_operator g) :
is_compact_operator (f - g)
def
compact_operator
{R₁ : Type u_1}
{R₄ : Type u_4}
[semiring R₁]
[comm_semiring R₄]
(σ₁₄ : R₁ →+* R₄)
(M₁ : Type u_5)
(M₄ : Type u_8)
[topological_space M₁]
[add_comm_monoid M₁]
[topological_space M₄]
[add_comm_group M₄]
[module R₁ M₁]
[module R₄ M₄]
[has_continuous_const_smul R₄ M₄]
[topological_add_group M₄] :
The submodule of compact continuous linear maps.
theorem
is_compact_operator.comp_clm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[topological_space M₁]
[topological_space M₂]
[topological_space M₃]
[add_comm_monoid M₁]
[module R₁ M₁]
[add_comm_monoid M₂]
[module R₂ M₂]
{f : M₂ → M₃}
(hf : is_compact_operator f)
(g : M₁ →SL[σ₁₂] M₂) :
is_compact_operator (f ∘ ⇑g)
theorem
is_compact_operator.continuous_comp
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[topological_space M₁]
[topological_space M₂]
[topological_space M₃]
[add_comm_monoid M₁]
{f : M₁ → M₂}
(hf : is_compact_operator f)
{g : M₂ → M₃}
(hg : continuous g) :
is_compact_operator (g ∘ f)
theorem
is_compact_operator.clm_comp
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₂]
[semiring R₃]
{σ₂₃ : R₂ →+* R₃}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[topological_space M₁]
[topological_space M₂]
[topological_space M₃]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R₂ M₂]
[add_comm_monoid M₃]
[module R₃ M₃]
{f : M₁ → M₂}
(hf : is_compact_operator f)
(g : M₂ →SL[σ₂₃] M₃) :
is_compact_operator (⇑g ∘ f)
theorem
is_compact_operator.cod_restrict
{R₂ : Type u_2}
[semiring R₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[topological_space M₂]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R₂ M₂]
{f : M₁ → M₂}
(hf : is_compact_operator f)
{V : submodule R₂ M₂}
(hV : ∀ (x : M₁), f x ∈ V)
(h_closed : is_closed ↑V) :
is_compact_operator (set.cod_restrict f ↑V hV)
theorem
is_compact_operator.restrict
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{f : M₁ →ₗ[R₁] M₁}
(hf : is_compact_operator ⇑f)
{V : submodule R₁ M₁}
(hV : ∀ (v : M₁), v ∈ V → ⇑f v ∈ V)
(h_closed : is_closed ↑V) :
is_compact_operator ⇑(f.restrict hV)
If a compact operator preserves a closed submodule, its restriction to that submodule is compact.
Note that, following mathlib's convention in linear algebra, restrict designates the restriction
of an endomorphism f : E →ₗ E to an endomorphism f' : ↥V →ₗ ↥V. To prove that the restriction
f' : ↥U →ₛₗ ↥V of a compact operator f : E →ₛₗ F is compact, apply
is_compact_operator.cod_restrict to f ∘ U.subtypeL, which is compact by
is_compact_operator.comp_clm.
theorem
is_compact_operator.restrict'
{R₂ : Type u_2}
[semiring R₂]
{M₂ : Type u_5}
[uniform_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
[separated_space M₂]
{f : M₂ →ₗ[R₂] M₂}
(hf : is_compact_operator ⇑f)
{V : submodule R₂ M₂}
(hV : ∀ (v : M₂), v ∈ V → ⇑f v ∈ V)
[hcomplete : complete_space ↥V] :
is_compact_operator ⇑(f.restrict hV)
If a compact operator preserves a complete submodule, its restriction to that submodule is compact.
Note that, following mathlib's convention in linear algebra, restrict designates the restriction
of an endomorphism f : E →ₗ E to an endomorphism f' : ↥V →ₗ ↥V. To prove that the restriction
f' : ↥U →ₛₗ ↥V of a compact operator f : E →ₛₗ F is compact, apply
is_compact_operator.cod_restrict to f ∘ U.subtypeL, which is compact by
is_compact_operator.comp_clm.
@[continuity]
theorem
is_compact_operator.continuous
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_group M₁]
[topological_space M₂]
[add_comm_group M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[topological_add_group M₁]
[has_continuous_const_smul 𝕜₁ M₁]
[topological_add_group M₂]
[has_continuous_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f) :
def
continuous_linear_map.mk_of_is_compact_operator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_group M₁]
[topological_space M₂]
[add_comm_group M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[topological_add_group M₁]
[has_continuous_const_smul 𝕜₁ M₁]
[topological_add_group M₂]
[has_continuous_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f) :
Upgrade a compact linear_map to a continuous_linear_map.
Equations
- continuous_linear_map.mk_of_is_compact_operator hf = {to_linear_map := f, cont := _}
@[simp]
theorem
continuous_linear_map.mk_of_is_compact_operator_to_linear_map
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_group M₁]
[topological_space M₂]
[add_comm_group M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[topological_add_group M₁]
[has_continuous_const_smul 𝕜₁ M₁]
[topological_add_group M₂]
[has_continuous_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f) :
@[simp]
theorem
continuous_linear_map.coe_mk_of_is_compact_operator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_group M₁]
[topological_space M₂]
[add_comm_group M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[topological_add_group M₁]
[has_continuous_const_smul 𝕜₁ M₁]
[topological_add_group M₂]
[has_continuous_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f) :
theorem
continuous_linear_map.mk_of_is_compact_operator_mem_compact_operator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[nontrivially_normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[ring_hom_isometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[topological_space M₁]
[add_comm_group M₁]
[topological_space M₂]
[add_comm_group M₂]
[module 𝕜₁ M₁]
[module 𝕜₂ M₂]
[topological_add_group M₁]
[has_continuous_const_smul 𝕜₁ M₁]
[topological_add_group M₂]
[has_continuous_smul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : is_compact_operator ⇑f) :
theorem
is_closed_set_of_is_compact_operator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[add_comm_group M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[uniform_space M₂]
[uniform_add_group M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
[complete_space M₂] :
is_closed {f : M₁ →SL[σ₁₂] M₂ | is_compact_operator ⇑f}
The set of compact operators from a normed space to a complete topological vector space is closed.
theorem
compact_operator_topological_closure
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[nontrivially_normed_field 𝕜₁]
[normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[seminormed_add_comm_group M₁]
[add_comm_group M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[uniform_space M₂]
[uniform_add_group M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
[complete_space M₂]
[has_continuous_smul 𝕜₂ (M₁ →SL[σ₁₂] M₂)] :
(compact_operator σ₁₂ M₁ M₂).topological_closure = compact_operator σ₁₂ M₁ M₂
theorem
is_compact_operator_of_tendsto
{ι : Type u_1}
{𝕜₁ : Type u_2}
{𝕜₂ : Type u_3}
[nontrivially_normed_field 𝕜₁]
[normed_field 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_4}
{M₂ : Type u_5}
[seminormed_add_comm_group M₁]
[add_comm_group M₂]
[normed_space 𝕜₁ M₁]
[module 𝕜₂ M₂]
[uniform_space M₂]
[uniform_add_group M₂]
[has_continuous_const_smul 𝕜₂ M₂]
[t2_space M₂]
[complete_space M₂]
{l : filter ι}
[l.ne_bot]
{F : ι → (M₁ →SL[σ₁₂] M₂)}
{f : M₁ →SL[σ₁₂] M₂}
(hf : filter.tendsto F l (nhds f))
(hF : ∀ᶠ (i : ι) in l, is_compact_operator ⇑(F i)) :