Filter.ptendsto'_def

theorem Filter.ptendsto'_def : ∀ {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β), Filter.PTendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁

The theorem `Filter.ptendsto'_def` states that for any types `α` and `β`, a partial function `f` from `α` to `β`, and filters `l₁` on `α` and `l₂` on `β`, the filter `l₁` tends to the filter `l₂` with respect to the partial function `f` (i.e., `Filter.PTendsto' f l₁ l₂`) if and only if for every set `s` that belongs to the filter `l₂`, the preimage of `s` under partial function `f`, denoted by `PFun.preimage f s`, belongs to the filter `l₁`. This theorem defines when a filter on the domain of a partial function tends to another filter on the codomain of the function.

More concisely: A filter `l₁` on a type `α` tends to a filter `l₂` on a type `β` with respect to a partial function `f:` `α` → `β` if and only if for every set `s` in `l₂`, the preimage `f⁁¹(s)` is in `l₁`.