α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91137
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ Filter.lift' (𝓤 α) interior
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91137
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α
rw [uniformity_eq_uniformity_interior]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91137
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ Filter.lift' (𝓤 α) interior
exact mem_lift' hs