English
Let f be a partially defined function with domain Dom(f). If Dom(f) belongs to the filter l1 and PTendsto f l1 l2 holds, then the primed version PTendsto' f l1 l2 also holds.
Русский
Пусть f — частично определенная функция с областью определения Dom(f). Если Dom(f) принадлежит фильтру l1 и выполняется PTendsto f l1 l2, то выполняется и PTendsto' f l1 l2.
LaTeX
$$$\forall f\, l_1\, l_2,\ (\operatorname{Dom} f \in l_1) \Rightarrow (\operatorname{PTendsto} f\ l_1\ l_2 \Rightarrow \operatorname{PTendsto}' f\ l_1\ l_2).$$$
Lean4
theorem ptendsto'_of_ptendsto {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} (h : f.Dom ∈ l₁) :
PTendsto f l₁ l₂ → PTendsto' f l₁ l₂ :=
by
rw [ptendsto_def, ptendsto'_def]
intro h' s sl₂
rw [PFun.preimage_eq]
exact inter_mem (h' s sl₂) h
