eventually_filterAt_iff — Mathlib

English

The tendsto and eventually characterization for filterAt: Tendsto f l (v.filterAt x) iff f eventually in setsAt x and containment in shrinking balls.

Русский

Характеризация предела по фильтру filterAt: Tendsto f l (v.filterAt x) эквивалентно тому, что f постепенно попадает в setsAt x и что f-elem уменьшаются в замкнутые шары.

LaTeX

$$$\\text{Tendsto}(f,l,v.filterAt x) \\iff (\\forall\\text{epsilon}>0)\\ (\\text{follows})$$$

Lean4

theorem eventually_filterAt_iff {x : X} {P : Set X → Prop} :
    (∀ᶠ t in v.filterAt x, P t) ↔ ∃ ε > (0 : ℝ), ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → P t :=
  v.mem_filterAt_iff

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