case a
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ uniformSpace α γ = ⨅ (i : ι), uniformSpace α γ
ext : 1
case a
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)
case a
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
change UniformFun.filter α γ 𝓤[⨅ i, u i] = 𝓤[⨅ i, 𝒰(α, γ, u i)]
case a
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)
case a
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)
rw [iInf_uniformity, iInf_uniformity]
no goals
case a
α : Type u_2
β : Type ?u.37540
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)
exact (UniformFun.gc α γ).u_iInf