α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (s : Set (β × β)), s ∈ 𝓤 β → (fun q => (f q.snd, F q.fst q.snd)) ⁻¹' s ∈ p ×ˢ 𝓟 {x}) ↔
    ∀ (s : Set (β × β)), s ∈ 𝓤 β → (fun x_1 => (f x, F x_1 x)) ⁻¹' s ∈ p
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n => F n x) p (𝓝 (f x))
simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (s : Set (β × β)), s ∈ 𝓤 β → (fun q => (f q.snd, F q.fst q.snd)) ⁻¹' s ∈ p ×ˢ 𝓟 {x}) ↔
    ∀ (s : Set (β × β)), s ∈ 𝓤 β → (fun x_1 => (f x, F x_1 x)) ⁻¹' s ∈ p
exact forall₂_congr fun u _ => by simp [mem_prod_principal, preimage]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (fun q => (f q.snd, F q.fst q.snd)) ⁻¹' u ∈ p ×ˢ 𝓟 {x} ↔ (fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p
simp [mem_prod_principal, preimage]