α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
⊢ ⋂₀ (𝓤 α).sets = ⋂ (i : ι) (_ : p i), s i
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
⊢ 𝓢 α = ⋂ (i : ι) (_ : p i), s i
unfold separationRel
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
⊢ ⋂₀ (𝓤 α).sets = ⋂ (i : ι) (_ : p i), s i
rw [h.sInter_sets]