Noncompact

Supporting results for the classification of compact one-dimensional manifolds.

theorem OneMfld.not_isCompact_Ici_zero_real : ¬IsCompact (Set.Ici 0)

[0, ∞) ⊆ ℝ is not compact.

theorem OneMfld.not_compactSpace_NNReal : ¬CompactSpace NNReal

NNReal (the nonnegative reals with the induced topology) is not a compact space.