eventually_filterAt_subset_closedBall

English

For x and ε>0, eventually in v.filterAt x, t ⊆ closedBall(x, ε).

Русский

Для x и ε>0 почти наверняка в v.filterAt x множество t ⊆ замкнутый шар вокруг x радиуса ε.

LaTeX

$$$$ \\forall x, \\forall \\varepsilon>0, \\forall t \\in v.filterAt x, t \\subseteq \\overline{B}(x,\\varepsilon) $$$$

Lean4

theorem eventually_filterAt_subset_closedBall (x : X) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ t : Set X in v.filterAt x, t ⊆ closedBall x ε :=
  (v.tendsto_filterAt_iff.mp tendsto_id).2 ε hε

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