tendsto_iff_ptendsto_univ — Mathlib

English

The Tendsto condition is equivalent to Tendsto with the universal set (univ) in the right-hand side of the res-predicate.

Русский

Условие сходимости эквивалентно сходимости с единичным множеством на правой стороне предиката res.

LaTeX

$$$ \\mathrm{Tendsto}\\, f\\, l_1\\, l_2 \\iff \\mathrm{PTendsto}\\, (\\mathrm{PFun.res}\\ f\\ \\mathrm{Set.univ})\\ l_1\\ l_2 $$$

Lean4

theorem tendsto_iff_ptendsto_univ (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
    Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂ :=
  by
  rw [← tendsto_iff_ptendsto]
  simp [principal_univ]

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