tendsto_iff_rtendsto' — Mathlib

English

Tendsto f l1 l2 is equivalent to RTendsto' (graph f) l1 l2.

Русский

Предел функции равен предельному поведению относительно графика: Tendsto f l1 l2 ⇔ RTendsto' (graph f) l1 l2.

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.preimage, Set.preimage]

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