α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.143853
s : Set (UniformSpace α)
⊢ UniformSpace.toTopologicalSpace = ⨅ (i : UniformSpace α) (_ : i ∈ s), UniformSpace.toTopologicalSpace
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.143853
s : Set (UniformSpace α)
⊢ UniformSpace.toTopologicalSpace = ⨅ (i : UniformSpace α) (_ : i ∈ s), UniformSpace.toTopologicalSpace
rw [sInf_eq_iInf]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.143853
s : Set (UniformSpace α)
⊢ UniformSpace.toTopologicalSpace = ⨅ (i : UniformSpace α) (_ : i ∈ s), UniformSpace.toTopologicalSpace
simp only [← toTopologicalSpace_iInf]