τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.22929
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.22929
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun t x => ϕ (m t) x) s ⊆ ω f₂ ϕ s
refine' iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, _⟩
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.22929
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 ϕ ((fun t => m t) '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.22929
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)
rw [← image2_image_left]
no goals
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.22929
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 ϕ ((fun t => m t) '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)
exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)