α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂
rw [← tendsto_iff_ptendsto]
no goals
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
simp [principal_univ]