English
Every compact operator between normed spaces is continuous.
Русский
Каждый компактный оператор между нормированными пространствами непрерывен.
LaTeX
$$$\\mathrm{IsCompactOperator}(f) \\Rightarrow \\mathrm{Continuous}(f).$$$
Lean4
@[continuity]
theorem continuous {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) : Continuous f :=
by
letI : UniformSpace M₂ := IsTopologicalAddGroup.toUniformSpace _
haveI : IsUniformAddGroup M₂ := isUniformAddGroup_of_addCommGroup
refine continuous_of_continuousAt_zero f fun U hU => ?_
rw [map_zero] at hU
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`.
rcases (hK.totallyBounded.isVonNBounded 𝕜₂ hU).exists_pos with
⟨r, hr, hrU⟩
-- Choose `c : 𝕜₂` with `r < ‖c‖`.
rcases NormedField.exists_lt_norm 𝕜₁ r with ⟨c, hc⟩
have hcnz : c ≠ 0 := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm
suffices (σ₁₂ <| c⁻¹) • K ⊆ U by
refine mem_of_superset ?_ this
have : IsUnit c⁻¹ := hcnz.isUnit.inv
rwa [mem_map, this.preimage_smul_setₛₗ σ₁₂, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)]
-- Since `σ₁₂ c⁻¹` = `(σ₁₂ c)⁻¹`, we have to prove that `K ⊆ σ₁₂ c • U`.
rw [map_inv₀, ← subset_smul_set_iff₀ ((map_ne_zero σ₁₂).mpr hcnz)]
-- But `σ₁₂` is isometric, so `‖σ₁₂ c‖ = ‖c‖ > r`, which concludes the argument since
-- `∀ a : 𝕜₂, r ≤ ‖a‖ → K ⊆ a • U`.
refine hrU (σ₁₂ c) ?_
rw [RingHomIsometric.norm_map]
exact hc.le
