α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (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 : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
⊢ UniformCauchySeqOnFilter F 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 : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (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 : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
have := (hf u hu).filter_mono (p'.prod_mono_left (Filter.prod_mono hp hp))
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
exact this.mono (by simp)
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
⊢ ∀ (x : (ι × ι) × α), (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u → (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
simp