α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p => (F p.fst x, F p.snd x)) (p ×ˢ p) (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy (map (fun i => F i x) p)
simp only [cauchy_map_iff, hp, true_and_iff]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ u ∈ map (fun p => (F p.fst x, F p.snd x)) (p ×ˢ p)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p => (F p.fst x, F p.snd x)) (p ×ˢ p) (𝓤 β)
intro u hu
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun p => (F p.fst x, F p.snd x)) ⁻¹' u ∈ p ×ˢ p
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ u ∈ map (fun p => (F p.fst x, F p.snd x)) (p ×ˢ p)
rw [mem_map]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun p => (F p.fst x, F p.snd x)) ⁻¹' u ∈ p ×ˢ p
filter_upwards [hf u hu]with p hp using hp x hx