ptendsto_iff_rtendsto — Mathlib

English

Tendsto f between filters is equivalent to RTendsto of its graph.

Русский

Предел функции между фильтрами эквивалентен RTendsto графика функции.

LaTeX

$$$ \\mathrm{Tendsto}\\, f\\, l_1\\, l_2 \\iff \\mathrm{RTendsto}\\, (\\mathrm{Function.graph}\\, f)\\, l_1\\, l_2 $$$

Lean4

theorem ptendsto_iff_rtendsto (l₁ : Filter α) (l₂ : Filter β) (f : α →. β) :
    PTendsto f l₁ l₂ ↔ RTendsto f.graph' l₁ l₂ :=
  Iff.rfl

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