tendsto_iff_rtendsto — Mathlib

English

Tendsto f between filters l1 and l2 is equivalent to the relation-based limit of the graph of f: the standard notion of convergence of f corresponds 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 tendsto_iff_rtendsto (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
    Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂ := by
  simp [tendsto_def, Function.graph, rtendsto_def, SetRel.core, Set.preimage]

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