Compactness

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

theorem OneMfld.clopen_in_r (s : Set NNReal) : s ≠ ∅ ∧ s ≠ Set.univ → ¬IsClopen s

theorem OneMfld.noncompact_nnreal : NoncompactSpace NNReal

theorem OneMfld.noncompact_ioo' (x y : NNReal) (hxy : x < y) : NoncompactSpace ↑(Set.Ioo x y)

theorem OneMfld.noncompact_ioo (x y : NNReal) (hxy : x < y) : ¬CompactSpace ↑(Set.Ioo x y)

theorem OneMfld.noncompact_iio' (x : NNReal) (hx : 0 < x) : NoncompactSpace ↑(Set.Iio x)

theorem OneMfld.noncompact_iio (x : NNReal) (hx : 0 < x) : ¬CompactSpace ↑(Set.Iio x)

theorem OneMfld.noncompact_target {M : Type u_1} [TopologicalSpace M] (ht : FinitelyIntervalChartedSpace M) (z : M) (a : OpenPartialHomeomorph M NNReal) (ha : a ∈ ChartedSpace.atlas) (hz : z ∈ a.source) : ¬CompactSpace ↑a.target