Theorems · Definition · general topology

Filter.Tendsto

{α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → Filter β → Prop

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.

Defined in

Mathlib.Order.Filter.Defs

Cited by

3,814 results in Mathlib

Foundations

Depth 13 from the axioms, rests on 73 definitions · uses propext, Quot.sound