α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
s' : Set α
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
s' : Set α
hf : UniformCauchySeqOn F p s
hss' : s' ⊆ s
⊢ UniformCauchySeqOn F p s'
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf⊢
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
s' : Set α
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')
exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')