ClassifyInterval

Classification of connected open subsets of the nonnegative real numbers.

theorem OneMfld.classify_connected_nnreal_interval (U : Set NNReal) (hu : IsOpen U) (hc : IsConnected U) : (∃ (x : NNReal) (y : NNReal), Set.Ioo x y = U) ∨ (∃ (x : NNReal), Set.Iio x = U) ∨ (∃ (x : NNReal), Set.Ioi x = U) ∨ U = Set.univ