eventually_nhds_norm_smul_sub_lt — Mathlib

English

For any c ∈ 𝕜, x ∈ E, and ε > 0, eventually near x we have ‖c • (y − x)‖ < ε.

Русский

Для любого c ∈ 𝕜, x ∈ E и ε > 0 существует окрестность x такого, что для любых y в этой окрестности выполнено ‖c·(y−x)‖ < ε.

LaTeX

$$$\\forall x \\in E, \\forall ε>0, \\exists neighbourhood\, U \, s.t. \\forall y \\in U, \\|c \\cdot (y - x)\\| < ε$$$

Lean4

theorem eventually_nhds_norm_smul_sub_lt (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) : ∀ᶠ y in 𝓝 x, ‖c • (y - x)‖ < ε :=
  have : Tendsto (fun y ↦ ‖c • (y - x)‖) (𝓝 x) (𝓝 0) := Continuous.tendsto' (by fun_prop) _ _ (by simp)
  this.eventually (gt_mem_nhds h)

Похожие утверждения