feat(topology): define class [noncompact_space] (#9839)

src/topology/alexandroff.lean

@@ -247,12 +247,12 @@ begin
 end
 
 /-- If `X` is a non-compact space, then `∞` is not an isolated point of `alexandroff X`. -/
-instance nhds_within_compl_infty_ne_bot [ne_bot (cocompact X)] :
+instance nhds_within_compl_infty_ne_bot [noncompact_space X] :
   ne_bot (𝓝[{∞}ᶜ] (∞ : alexandroff X)) :=
 by { rw nhds_within_compl_infty_eq, apply_instance }
 
 @[priority 900]
-instance nhds_within_compl_ne_bot [∀ x : X, ne_bot (𝓝[{x}ᶜ] x)] [ne_bot (cocompact X)]
+instance nhds_within_compl_ne_bot [∀ x : X, ne_bot (𝓝[{x}ᶜ] x)] [noncompact_space X]
   (x : alexandroff X) : ne_bot (𝓝[{x}ᶜ] x) :=
 alexandroff.rec _ alexandroff.nhds_within_compl_infty_ne_bot
   (λ y, alexandroff.nhds_within_compl_coe_ne_bot y) x
@@ -306,14 +306,14 @@ by rw [continuous_at, nhds_coe_eq, tendsto_map'_iff, continuous_at]
 
 /-- If `X` is not a compact space, then the natural embedding `X → alexandroff X` has dense range.
 -/
-lemma dense_range_coe [ne_bot (cocompact X)] :
+lemma dense_range_coe [noncompact_space X] :
   dense_range (coe : X → alexandroff X) :=
 begin
   rw [dense_range, ← compl_infty],
   exact dense_compl_singleton _
 end
 
-lemma dense_embedding_coe [ne_bot (cocompact X)] :
+lemma dense_embedding_coe [noncompact_space X] :
   dense_embedding (coe : X → alexandroff X) :=
 { dense := dense_range_coe, .. open_embedding_coe }
 
@@ -391,7 +391,7 @@ begin
 end
 
 /-- If `X` is not a compact space, then `alexandroff X` is a connected space. -/
-instance [preconnected_space X] [ne_bot (cocompact X)] : connected_space (alexandroff X) :=
+instance [preconnected_space X] [noncompact_space X] : connected_space (alexandroff X) :=
 { to_preconnected_space := dense_embedding_coe.to_dense_inducing.preconnected_space,
   to_nonempty := infer_instance }
 

src/topology/instances/real.lean

@@ -98,8 +98,19 @@ instance : proper_space ℤ :=
     exact (set.finite_Icc _ _).is_compact,
   end ⟩
 
+instance : noncompact_space ℤ :=
+begin
+  rw [← not_compact_space_iff, metric.compact_space_iff_bounded_univ],
+  rintro ⟨r, hr⟩,
+  refine (hr (⌊r⌋ + 1) 0 trivial trivial).not_lt _,
+  simpa [dist_eq] using (lt_floor_add_one r).trans_le (le_abs_self _)
+end
+
 end int
 
+instance : noncompact_space ℚ := int.closed_embedding_coe_rat.noncompact_space
+instance : noncompact_space ℝ := int.closed_embedding_coe_real.noncompact_space
+
 theorem real.uniform_continuous_add : uniform_continuous (λp : ℝ × ℝ, p.1 + p.2) :=
 metric.uniform_continuous_iff.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0 in

src/topology/metric_space/basic.lean

@@ -1856,6 +1856,18 @@ iff.intro
 lemma bounded.ediam_ne_top (h : bounded s) : emetric.diam s ≠ ⊤ :=
 bounded_iff_ediam_ne_top.1 h
 
+lemma ediam_univ_eq_top_iff_noncompact [proper_space α] :
+  emetric.diam (univ : set α) = ∞ ↔ noncompact_space α :=
+by rw [← not_compact_space_iff, compact_space_iff_bounded_univ, bounded_iff_ediam_ne_top, not_not]
+
+@[simp] lemma ediam_univ_of_noncompact [proper_space α] [noncompact_space α] :
+  emetric.diam (univ : set α) = ∞ :=
+ediam_univ_eq_top_iff_noncompact.mpr ‹_›
+
+@[simp] lemma diam_univ_of_noncompact [proper_space α] [noncompact_space α] :
+  diam (univ : set α) = 0 :=
+by simp [diam]
+
 /-- The distance between two points in a set is controlled by the diameter of the set. -/
 lemma dist_le_diam_of_mem (h : bounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s :=
 dist_le_diam_of_mem' h.ediam_ne_top hx hy

src/topology/subset_properties.lean

@@ -28,10 +28,11 @@ For each of these definitions (except for `is_clopen`), we also have a class sta
 space satisfies that property:
 `compact_space`, `irreducible_space`
 
-Furthermore, we have two more classes:
+Furthermore, we have three more classes:
 * `locally_compact_space`: for every point `x`, every open neighborhood of `x` contains a compact
   neighborhood of `x`. The definition is formulated in terms of the neighborhood filter.
-* `sigma_compact_space`: a space that is the union of a countably many compact subspaces.
+* `sigma_compact_space`: a space that is the union of a countably many compact subspaces;
+* `noncompact_space`: a space that is not a compact space.
 
 ## On the definition of irreducible and connected sets/spaces
 
@@ -582,27 +583,30 @@ lemma is_closed.is_compact [compact_space α] {s : set α} (h : is_closed s) :
   is_compact s :=
 compact_of_is_closed_subset compact_univ h (subset_univ _)
 
-lemma filter.cocompact_ne_bot_tfae (α : Type*) [topological_space α] :
-  tfae [ne_bot (filter.cocompact α),
-    ne_bot (filter.coclosed_compact α),
-    ¬is_compact (univ : set α),
-    ¬compact_space α] :=
+/-- `α` is a noncompact topological space if it not a compact space. -/
+class noncompact_space (α : Type*) [topological_space α] : Prop :=
+(noncompact_univ [] : ¬is_compact (univ : set α))
+
+export noncompact_space (noncompact_univ)
+
+instance [noncompact_space α] : ne_bot (filter.cocompact α) :=
 begin
-  tfae_have : 1 → 2, from λ h, h.mono filter.cocompact_le_coclosed_compact,
-  tfae_have : 3 ↔ 4, from not_congr is_compact_univ_iff,
-  tfae_have : 2 → 3, from λ h₁ h₂, (filter.has_basis_coclosed_compact.ne_bot_iff.1 h₁
-    ⟨is_closed_univ, h₂⟩).ne_empty compl_univ,
-  tfae_have : 3 → 1,
-  { refine λ h₁, filter.has_basis_cocompact.ne_bot_iff.2 (λ s hs, _),
-    contrapose! h₁, rw [not_nonempty_iff_eq_empty, compl_empty_iff] at h₁,
-    rwa ← h₁ },
-  tfae_finish
+  refine filter.has_basis_cocompact.ne_bot_iff.2 (λ s hs, _),
+  contrapose hs, rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs,
+  rw hs, exact noncompact_univ α
 end
 
-/-- `ne_bot (cocompact α)` is the canonical way to say that `α` is not a compact space using
-typeclasses. -/
-instance [ne_bot (filter.cocompact α)] : ne_bot (filter.coclosed_compact α) :=
-((filter.cocompact_ne_bot_tfae α).out 0 1).mp ‹_›
+instance [noncompact_space α] : ne_bot (filter.coclosed_compact α) :=
+ne_bot_of_le filter.cocompact_le_coclosed_compact
+
+lemma noncompact_space_of_ne_bot (h : ne_bot (filter.cocompact α)) : noncompact_space α :=
+⟨λ h', (filter.nonempty_of_mem h'.compl_mem_cocompact).ne_empty compl_univ⟩
+
+lemma filter.cocompact_ne_bot_iff : ne_bot (filter.cocompact α) ↔ noncompact_space α :=
+⟨noncompact_space_of_ne_bot, @filter.cocompact.filter.ne_bot _ _⟩
+
+lemma not_compact_space_iff : ¬compact_space α ↔ noncompact_space α :=
+⟨λ h₁, ⟨λ h₂, h₁ ⟨h₂⟩⟩, λ ⟨h₁⟩ ⟨h₂⟩, h₁ h₂⟩
 
 /-- A compact discrete space is finite. -/
 noncomputable
@@ -752,6 +756,14 @@ by rw [compact_iff_compact_in_subtype, image_univ, subtype.range_coe]; refl
 lemma is_compact_iff_compact_space {s : set α} : is_compact s ↔ compact_space s :=
 is_compact_iff_is_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.compact_univ _ _⟩
 
+protected lemma closed_embedding.noncompact_space [noncompact_space α] {f : α → β}
+  (hf : closed_embedding f) : noncompact_space β :=
+noncompact_space_of_ne_bot hf.tendsto_cocompact.ne_bot
+
+protected lemma closed_embedding.compact_space [h : compact_space β] {f : α → β}
+  (hf : closed_embedding f) : compact_space α :=
+by { unfreezingI { contrapose! h, rw not_compact_space_iff at h ⊢ }, exact hf.noncompact_space }
+
 lemma is_compact.prod {s : set α} {t : set β} (hs : is_compact s) (ht : is_compact t) :
   is_compact (set.prod s t) :=
 begin
@@ -801,7 +813,7 @@ end⟩
 
 /-- The coproduct of the cocompact filters on two topological spaces is the cocompact filter on
 their product. -/
-lemma filter.coprod_cocompact {β : Type*} [topological_space β]:
+lemma filter.coprod_cocompact :
   (filter.cocompact α).coprod (filter.cocompact β) = filter.cocompact (α × β) :=
 begin
   ext S,
@@ -827,6 +839,18 @@ begin
       exact subset.trans htS (subset_preimage_image prod.snd _) } }
 end
 
+lemma prod.noncompact_space_iff :
+  noncompact_space (α × β) ↔ noncompact_space α ∧ nonempty β ∨ nonempty α ∧ noncompact_space β :=
+by simp [← filter.cocompact_ne_bot_iff, ← filter.coprod_cocompact, filter.coprod_ne_bot_iff]
+
+@[priority 100] -- See Note [lower instance priority]
+instance prod.noncompact_space_left [noncompact_space α] [nonempty β] : noncompact_space (α × β) :=
+prod.noncompact_space_iff.2 (or.inl ⟨‹_›, ‹_›⟩)
+
+@[priority 100] -- See Note [lower instance priority]
+instance prod.noncompact_space_right [nonempty α] [noncompact_space β] : noncompact_space (α × β) :=
+prod.noncompact_space_iff.2 (or.inr ⟨‹_›, ‹_›⟩)
+
 section tychonoff
 variables {ι : Type*} {π : ι → Type*} [∀ i, topological_space (π i)]