ptendsto_of_ptendsto' — Mathlib

English

From PTendsto' we can derive PTendsto: if PTendsto' holds, then PTendsto holds for the same data.

Русский

Из PTendsto' следует PTendsto; если выполнено PTendsto', то выполняется PTendsto.

LaTeX

$$$ \\mathrm{PTendsto}'\\ f\\ l_1\\ l_2 \\rightarrow \\mathrm{PTendsto}\\ f\\ l_1\\ l_2 $$$

Lean4

theorem ptendsto_of_ptendsto' {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} : PTendsto' f l₁ l₂ → PTendsto f l₁ l₂ :=
  by
  rw [ptendsto_def, ptendsto'_def]
  exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)

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