α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s₁, s₂})
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)
rw [← sUnion_pair]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s₁, s₂})
refine' tendstoLocallyUniformlyOn_sUnion _ _ _ <;> simp [*]