α : Type u_1
β : Type u_2
γ : Type ?u.57789
ι : Type ?u.57792
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ (⨅ (i : Set α) (_ : i ∈ 𝔖), TopologicalSpace.induced (restrict i) UniformSpace.toTopologicalSpace) =
    ⨅ (s : Set α) (_ : s ∈ 𝔖),
      TopologicalSpace.induced (restrict s ∘ ↑UniformFun.toFun) (UniformFun.topologicalSpace (↑s) β)
α : Type u_1
β : Type u_2
γ : Type ?u.57789
ι : Type ?u.57792
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ topologicalSpace α β 𝔖 =
    ⨅ (s : Set α) (_ : s ∈ 𝔖),
      TopologicalSpace.induced (restrict s ∘ ↑UniformFun.toFun) (UniformFun.topologicalSpace (↑s) β)
simp only [UniformOnFun.topologicalSpace, toTopologicalSpace_iInf, toTopologicalSpace_iInf,
  toTopologicalSpace_comap]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.57789
ι : Type ?u.57792
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ (⨅ (i : Set α) (_ : i ∈ 𝔖), TopologicalSpace.induced (restrict i) UniformSpace.toTopologicalSpace) =
    ⨅ (s : Set α) (_ : s ∈ 𝔖),
      TopologicalSpace.induced (restrict s ∘ ↑UniformFun.toFun) (UniformFun.topologicalSpace (↑s) β)
rfl