Topology lemma for ENat.toENNReal

This file shows ENat.toENNReal is a closed embedding.

theorem ENat.continuous_toENNReal : Continuous toENNReal

theorem ENat.isClosedEmbedding_toENNReal : Topology.IsClosedEmbedding toENNReal