PTendsto — Mathlib

English

A simplification form of the membership statement for pmap: membership is equivalent to membership of the core under the original filter.

Русский

Упрощенная форма леммы о принадлежности в pmap: принадлежность эквивалентна принадлежности ядра в исходном фильтре.

LaTeX

$$$ s \\in l.pmap f \\iff f.core s \\in l $$$

Lean4

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

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