α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ u) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.snd, F n.fst n.snd) ∈ u
α : 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 s ↔ TendstoUniformlyOnFilter F f p (𝓟 s)
simp only [TendstoUniformlyOn, TendstoUniformlyOnFilter]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ ∀ (a : Set (β × β)),
    a ∈ 𝓤 β →
      ((∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ a) ↔
        ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.snd, F n.fst n.snd) ∈ a)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ u) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.snd, F n.fst n.snd) ∈ u
apply forall₂_congr
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ ∀ (a : Set (β × β)), a ∈ 𝓤 β → True
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ ∀ (a : Set (β × β)),
    a ∈ 𝓤 β →
      ((∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ a) ↔
        ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.snd, F n.fst n.snd) ∈ a)
simp_rw [eventually_prod_principal_iff]
no goals
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ ∀ (a : Set (β × β)), a ∈ 𝓤 β → True
simp