α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
⊢ (∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → PFun.preimage f s ∈ l₁
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
⊢ PTendsto f l₁ l₂ → PTendsto' f l₁ l₂
rw [ptendsto_def, ptendsto'_def]
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
h' : ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ PFun.preimage f s ∈ l₁
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
⊢ (∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁) → ∀ (s : Set β), s ∈ l₂ → PFun.preimage f s ∈ l₁
intro h' s sl₂
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
h' : ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ PFun.core f s ∩ PFun.Dom f ∈ l₁
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
h' : ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ PFun.preimage f s ∈ l₁
rw [PFun.preimage_eq]
no goals
α : Type u
β : Type v
γ : Type w
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : PFun.Dom f ∈ l₁
h' : ∀ (s : Set β), s ∈ l₂ → PFun.core f s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ PFun.core f s ∩ PFun.Dom f ∈ l₁
exact inter_mem (h' s sl₂) h