α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)
simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u) ↔
    ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
refine' forall₂_congr fun u hu => _
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 (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u) ↔
    ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
rw [eventually_prod_principal_iff]