α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → PFun.preimage f s ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto' f l₁ l₂ → PTendsto f l₁ l₂
rw [ptendsto_def, ptendsto'_def]
no goals
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → PFun.preimage f s ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)