no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.315768
ι : Sort x
f : α → β
x₁ x₂ : Filter α
y : Filter β
⊢ Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y
simp only [Tendsto, map_sup, sup_le_iff]