English
If s is bounded, then for small enough r, the set {x} + r·s is contained in any neighborhood of x.
Русский
Если s ограничено, то для sufficiently малого r множество {x} + r·s входит в любую окрестность x.
LaTeX
$$$\forall x,s\; (\mathrm{IsBounded}\,s) \to \exists \epsilon>0, \forall r\in B(0,\epsilon):\{x\}+r·s \subseteq U.$$$
Lean4
/-- If `s` is a bounded set, then for small enough `r`, the set `{x} + r • s` is contained in any
fixed neighborhood of `x`. -/
theorem eventually_singleton_add_smul_subset {x : E} {s : Set E} (hs : Bornology.IsBounded s) {u : Set E}
(hu : u ∈ 𝓝 x) : ∀ᶠ r in 𝓝 (0 : 𝕜), { x } + r • s ⊆ u :=
by
obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
obtain ⟨R, Rpos, hR⟩ : ∃ R : ℝ, 0 < R ∧ s ⊆ closedBall 0 R := hs.subset_closedBall_lt 0 0
have : Metric.closedBall (0 : 𝕜) (ε / R) ∈ 𝓝 (0 : 𝕜) := closedBall_mem_nhds _ (div_pos εpos Rpos)
filter_upwards [this] with r hr
simp only [image_add_left, singleton_add]
intro y hy
obtain ⟨z, zs, hz⟩ : ∃ z : E, z ∈ s ∧ r • z = -x + y := by simpa [mem_smul_set] using hy
have I : ‖r • z‖ ≤ ε :=
calc
‖r • z‖ = ‖r‖ * ‖z‖ := norm_smul _ _
_ ≤ ε / R * R :=
(mul_le_mul (mem_closedBall_zero_iff.1 hr) (mem_closedBall_zero_iff.1 (hR zs)) (norm_nonneg _)
(div_pos εpos Rpos).le)
_ = ε := by field_simp
have : y = x + r • z := by simp only [hz, add_neg_cancel_left]
apply hε
simpa only [this, dist_eq_norm, add_sub_cancel_left, mem_closedBall] using I
