α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x => ↑(toFun 𝔖) x i
α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous ↑(toFun 𝔖)
rw [uniformContinuous_pi]
α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
⊢ UniformContinuous fun x_1 => ↑(toFun 𝔖) x_1 x
α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x => ↑(toFun 𝔖) x i
intro x
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s✝ s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous fun x_1 => ↑(toFun 𝔖) x_1 x
α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
⊢ UniformContinuous fun x_1 => ↑(toFun 𝔖) x_1 x
obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := sUnion_eq_univ_iff.mp h x
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.103188
ι : Type ?u.103191
s✝ s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous fun x_1 => ↑(toFun 𝔖) x_1 x
exact uniformContinuous_eval_of_mem β 𝔖 hxs hs