tendsto_iff_ultrafilter — Mathlib

English

The Tendsto relation can be checked on ultrafilters: Tendsto f l1 l2 holds iff for every ultrafilter g on α with g ≤ l1, Tendsto f g l2.

Русский

Связь Tendsto может проверяться на ультрафильтрах: Tendsto f l1 l2 эквивалентно тому, что для каждого ультрафильтра g на α с g ≤ l1 выполняется Tendsto f g l2.

LaTeX

$$$\mathrm{Tendsto}\, f\, l_1\, l_2 \iff \forall g:\mathrm{Ultrafilter}\, α,\; g\le l_1 \Rightarrow \mathrm{Tendsto}\, f\, g\, l_2$$

Lean4

/-- The `tendsto` relation can be checked on ultrafilters. -/
theorem tendsto_iff_ultrafilter (f : α → β) (l₁ : Filter α) (l₂ : Filter β) :
    Tendsto f l₁ l₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ l₁ → Tendsto f g l₂ := by
  simpa only [tendsto_iff_comap] using le_iff_ultrafilter

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