tendsto_filterAt_iff — Mathlib

English

A general tendsto criterion for Vitali filter: Tendsto f l (v.filterAt x) iff appropriate eventual membership and containment in closed balls.

Русский

Общее условие предела для фильтра Vitali: Tendsto f l (v.filterAt x) если и только если существует нужное моментальное membership и вложение в замкнутые шары.

LaTeX

$$$\\text{Tendsto}(f,l,v.filterAt x)\\iff \\dots$$$

Lean4

theorem tendsto_filterAt_iff {ι : Type*} {l : Filter ι} {f : ι → Set X} {x : X} :
    Tendsto f l (v.filterAt x) ↔ (∀ᶠ i in l, f i ∈ v.setsAt x) ∧ ∀ ε > (0 : ℝ), ∀ᶠ i in l, f i ⊆ closedBall x ε := by
  simp only [filterAt, tendsto_inf, nhds_basis_closedBall.smallSets.tendsto_right_iff, tendsto_principal, and_comm,
    mem_powerset_iff]

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