English
If hb holds and hc provides closed image, the image is compact.
Русский
Если hb выполняется и hc обеспечивает замкнутый образ, образ компактный.
LaTeX
$$$\\mathrm{IsCompact}\\left( ((\\uparrow) : (E' \\toSL[\\sigma_{12}] F) \\to E' \\to F) '' s \\right)$$$
Lean4
/-- A closed ball is closed in the weak-* topology. We don't have a name for `E →SL[σ] F` with
weak-* topology in `mathlib`, so we use an equivalent condition (see `isClosed_induced_iff'`). -/
theorem is_weak_closed_closedBall (f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄
(hf : ⇑f ∈ closure (((↑) : (E' →SL[σ₁₂] F) → E' → F) '' closedBall f₀ r)) : f ∈ closedBall f₀ r :=
by
have hr : 0 ≤ r := nonempty_closedBall.1 (closure_nonempty_iff.1 ⟨_, hf⟩).of_image
refine mem_closedBall_iff_norm.2 (opNorm_le_bound _ hr fun x => ?_)
have : IsClosed {g : E' → F | ‖g x - f₀ x‖ ≤ r * ‖x‖} :=
isClosed_Iic.preimage ((@continuous_apply E' (fun _ => F) _ x).sub continuous_const).norm
refine this.closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf
exact (g - f₀).le_of_opNorm_le (mem_closedBall_iff_norm.1 hg) _
