theorem real_t2Space : T2Space ℝ

Text 1.0.50 (1): the real line with its usual metric topology is Hausdorff.

theorem real_not_compact : ¬CompactSpace ℝ

Text 1.0.50 (2): the real line with its usual topology is not compact.