Tendsto — Mathlib

English

Tendsto f l1 l2 is the statement that for every neighborhood of a in l2, the preimage under f is a neighborhood of l1; i.e., l1.map f ≤ l2.

Русский

Tendsto f l1 l2 означает, что для каждого окрестности a в l2 множество обратного образа f принадлежит l1; то есть l1.map f ≤ l2.

LaTeX

$$$\\mathrm{Tendsto}(f,l_1,l_2) \\iff l_1.map f \\le l_2$$$

Lean4

/-- `Filter.Tendsto` is the generic "limit of a function" predicate.
  `Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
  the `f`-preimage of `a` is an `l₁` neighborhood. -/
def Tendsto (f : α → β) (l₁ : Filter α) (l₂ : Filter β) :=
  l₁.map f ≤ l₂

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