PTendsto' — Mathlib

English

The predicate PTendsto' is defined as l1 ≤ l2.rcomap' f.graph'.

Русский

Predicat PTendsto' определяется как отношение включения фильтров: l1 ≤ l2.rcomap' f.graph'.

LaTeX

$$$ \\mathrm{PTendsto}'\\ f\\ l_1\\ l_2 := l_1 \\leq l_2.rcomap'\\ f.graph' $$$

Lean4

/-- Generic "limit of a partial function" predicate. `PTendsto' r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `p`-preimage of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to partial functions. -/
def PTendsto' (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :=
  l₁ ≤ l₂.rcomap' f.graph'

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