English
The range of the embedding toBCF is a closed subset of the space of bounded continuous maps.
Русский
Образ вложения toBCF является замкнутым подмножеством пространства ограниченных непрерывных отображений.
LaTeX
$$IsClosed(range(toBCF))$$
Lean4
theorem isClosed_range_toBCF : IsClosed (range (toBCF : C₀(α, β) → α →ᵇ β)) :=
by
refine isClosed_iff_clusterPt.mpr fun f hf => ?_
rw [clusterPt_principal_iff] at hf
have : Tendsto f (cocompact α) (𝓝 0) :=
by
refine Metric.tendsto_nhds.mpr fun ε hε => ?_
obtain ⟨_, hg, g, rfl⟩ := hf (ball f (ε / 2)) (ball_mem_nhds f <| half_pos hε)
refine (Metric.tendsto_nhds.mp (zero_at_infty g) (ε / 2) (half_pos hε)).mp (Eventually.of_forall fun x hx => ?_)
calc
dist (f x) 0 ≤ dist (g.toBCF x) (f x) + dist (g x) 0 := dist_triangle_left _ _ _
_ < dist g.toBCF f + ε / 2 := (add_lt_add_of_le_of_lt (dist_coe_le_dist x) hx)
_ < ε := by simpa [add_halves ε] using add_lt_add_right (mem_ball.1 hg) (ε / 2)
exact ⟨⟨f.toContinuousMap, this⟩, rfl⟩
