α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.snd, F n.fst n.snd) ∈ u ∧ F n.fst n.snd = F' n.fst n.snd
⊢ (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 : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
⊢ TendstoUniformlyOnFilter F' f p p'
refine' fun u hu => ((hf u hu).and hff').mono fun n h => _
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.snd, F n.fst n.snd) ∈ u ∧ F n.fst n.snd = F' n.fst n.snd
⊢ (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 : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.snd, F n.fst n.snd) ∈ u ∧ F n.fst n.snd = F' n.fst n.snd
⊢ (f n.snd, F' n.fst n.snd) ∈ u
rw [← h.right]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.snd, F n.fst n.snd) ∈ u ∧ F n.fst n.snd = F' n.fst n.snd
⊢ (f n.snd, F n.fst n.snd) ∈ u
exact h.left