α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsClosed (⋂₀ (closure '' (𝓤 α).sets))
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsClosed (𝓢 α)
rw [separationRel_eq_inter_closure]
case a
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ (t : Set (α × α)), t ∈ closure '' (𝓤 α).sets → IsClosed t
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ IsClosed (⋂₀ (closure '' (𝓤 α).sets))
apply isClosed_sInter
case a.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (α × α)
⊢ IsClosed (closure t)
case a
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ (t : Set (α × α)), t ∈ closure '' (𝓤 α).sets → IsClosed t
rintro _ ⟨t, -, rfl⟩
no goals
case a.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (α × α)
⊢ IsClosed (closure t)
exact isClosed_closure