ptendsto'_nhds — Mathlib

English

For partial maps f : Y ⇢ X, PTendsto' f l (nhds x) iff for all open s, x ∈ s implies f.preimage s ∈ l.

Русский

Для частичных отображений f : Y ⇢ X, PTendsto' f l (nhds x) эквивалентно: для всех открытых s, x ∈ s → f.preimage s ∈ l.

LaTeX

$$$\\mathrm{PTendsto'}\\,f\\,l\\,(\\mathcal{N}(x)) \\iff \\forall s, \\mathrm{IsOpen}s \\to x \\in s \\to f.preimage s \\in l$$$

Lean4

theorem ptendsto'_nhds {f : Y →. X} {l : Filter Y} {x : X} :
    PTendsto' f l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → f.preimage s ∈ l :=
  rtendsto'_nhds

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