α : Type ?u.6979
inst✝ : TopologicalSpace α
⊢ IsClosed (Ici 0)
α : Type ?u.6979
inst✝ : TopologicalSpace α
⊢ IsClosed (range ENNReal.toEReal)
rw [range_coe_ennreal]
no goals
α : Type ?u.6979
inst✝ : TopologicalSpace α
⊢ IsClosed (Ici 0)
exact isClosed_Ici