feat(topology/subset_properties): open/closed sets are locally compac…

…t spaces (#10844)

* add `inducing.image_mem_nhds_within`;
* move `inducing.is_compact_iff` up, use it to prove `embedding.is_compact_iff_is_compact_image`;
* prove `closed_embedding.is_compact_preimage`, use it to prove `closed_embedding.tendsto_cocompact`;
* prove `closed_embedding.locally_compact_space`, `open_embedding.locally_compact_space`;
* specialize to `is_closed.locally_compact_space`, `is_open.locally_compact_space`;
* rename `locally_finite.countable_of_sigma_compact` to `locally_finite.countable_univ`, provide `locally_finite.encodable`.

src/topology/maps.lean

@@ -81,10 +81,14 @@ lemma inducing.map_nhds_of_mem {f : α → β} (hf : inducing f) (a : α) (h : r
   (𝓝 a).map f = 𝓝 (f a) :=
 hf.induced.symm ▸ map_nhds_induced_of_mem h
 
+lemma inducing.image_mem_nhds_within {f : α → β} (hf : inducing f) {a : α} {s : set α}
+  (hs : s ∈ 𝓝 a) : f '' s ∈ 𝓝[range f] (f a) :=
+hf.map_nhds_eq a ▸ image_mem_map hs
+
 lemma inducing.tendsto_nhds_iff {ι : Type*}
   {f : ι → β} {g : β → γ} {a : filter ι} {b : β} (hg : inducing g) :
   tendsto f a (𝓝 b) ↔ tendsto (g ∘ f) a (𝓝 (g b)) :=
-by rw [tendsto, tendsto, hg.induced, nhds_induced, ← map_le_iff_le_comap, filter.map_map]
+by rw [hg.nhds_eq_comap, tendsto_comap_iff]
 
 lemma inducing.continuous_at_iff {f : α → β} {g : β → γ} (hg : inducing g) {x : α} :
   continuous_at f x ↔ continuous_at (g ∘ f) x :=
@@ -375,7 +379,7 @@ hf.to_embedding.to_inducing.is_open_map hf.open_range
 
 lemma open_embedding.map_nhds_eq {f : α → β} (hf : open_embedding f) (a : α) :
   map f (𝓝 a) = 𝓝 (f a) :=
-hf.to_embedding.map_nhds_of_mem _ $ is_open.mem_nhds hf.open_range $ mem_range_self _
+hf.to_embedding.map_nhds_of_mem _ $ hf.open_range.mem_nhds $ mem_range_self _
 
 lemma open_embedding.open_iff_image_open {f : α → β} (hf : open_embedding f)
   {s : set α} : is_open s ↔ is_open (f '' s) :=

src/topology/subset_properties.lean

@@ -721,31 +721,43 @@ lemma exists_subset_nhd_of_compact_space [compact_space α] {ι : Type*} [nonemp
   {U : set α} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U :=
 exists_subset_nhd_of_compact' hV (λ i, (hV_closed i).is_compact) hV_closed hU
 
+/-- If `f : α → β` is an `inducing` map, then the image `f '' s` of a set `s` is compact if and only
+if the set `s` is closed. -/
+lemma inducing.is_compact_iff {f : α → β} (hf : inducing f) {s : set α} :
+  is_compact (f '' s) ↔ is_compact s :=
+begin
+  refine ⟨_, λ hs, hs.image hf.continuous⟩,
+  introsI hs F F_ne_bot F_le,
+  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : cluster_pt (f x) (map f F)⟩ :=
+    hs (calc map f F ≤ map f (𝓟 s) : map_mono F_le
+                ... = 𝓟 (f '' s) : map_principal),
+  use [x, x_in],
+  suffices : (map f (𝓝 x ⊓ F)).ne_bot, by simpa [filter.map_ne_bot_iff],
+  rwa calc map f (𝓝 x ⊓ F) = map f ((comap f $ 𝓝 $ f x) ⊓ F) : by rw hf.nhds_eq_comap
+                        ... = 𝓝 (f x) ⊓ map f F : filter.push_pull' _ _ _
+end
+
+/-- If `f : α → β` is an `embedding` (or more generally, an `inducing` map, see
+`inducing.is_compact_iff`), then the image `f '' s` of a set `s` is compact if and only if the set
+`s` is closed. -/
 lemma embedding.is_compact_iff_is_compact_image {f : α → β} (hf : embedding f) :
   is_compact s ↔ is_compact (f '' s) :=
-iff.intro (assume h, h.image hf.continuous) $ assume h, begin
-  rw is_compact_iff_ultrafilter_le_nhds at ⊢ h,
-  intros u us',
-  have : ↑(u.map f) ≤ 𝓟 (f '' s), begin
-    rw [ultrafilter.coe_map, map_le_iff_le_comap, comap_principal], convert us',
-    exact preimage_image_eq _ hf.inj
-  end,
-  rcases h (u.map f) this with ⟨_, ⟨a, ha, ⟨⟩⟩, _⟩,
-  refine ⟨a, ha, _⟩,
-  rwa [hf.induced, nhds_induced, ←map_le_iff_le_comap]
+hf.to_inducing.is_compact_iff.symm
+
+/-- The preimage of a compact set under a closed embedding is a compact set. -/
+lemma closed_embedding.is_compact_preimage {f : α → β} (hf : closed_embedding f) {K : set β}
+  (hK : is_compact K) : is_compact (f ⁻¹' K) :=
+begin
+  replace hK := hK.inter_right hf.closed_range,
+  rwa [← hf.to_inducing.is_compact_iff, image_preimage_eq_inter_range]
 end
 
-/-- A closed embedding is proper, ie, inverse images of compact sets are contained in compacts. -/
+/-- A closed embedding is proper, ie, inverse images of compact sets are contained in compacts.
+Moreover, the preimage of a compact set is compact, see `closed_embedding.is_compact_preimage`. -/
 lemma closed_embedding.tendsto_cocompact
   {f : α → β} (hf : closed_embedding f) : tendsto f (filter.cocompact α) (filter.cocompact β) :=
-begin
-  rw filter.has_basis_cocompact.tendsto_iff filter.has_basis_cocompact,
-  intros K hK,
-  refine ⟨f ⁻¹' (K ∩ (set.range f)), _, λ x hx, by simpa using hx⟩,
-  apply hf.to_embedding.is_compact_iff_is_compact_image.mpr,
-  rw set.image_preimage_eq_of_subset (set.inter_subset_right _ _),
-  exact hK.inter_right hf.closed_range,
-end
+filter.has_basis_cocompact.tendsto_right_iff.mpr $ λ K hK,
+  (hf.is_compact_preimage hK).compl_mem_cocompact
 
 lemma compact_iff_compact_in_subtype {p : α → Prop} {s : set {a // p a}} :
   is_compact s ↔ is_compact ((coe : _ → α) '' s) :=
@@ -781,22 +793,6 @@ begin
   rw nhds_prod_eq, exact le_inf ha hb
 end
 
-lemma inducing.is_compact_iff {f : α → β} (hf : inducing f) {s : set α} :
-  is_compact (f '' s) ↔ is_compact s :=
-begin
-  split,
-  { introsI hs F F_ne_bot F_le,
-    obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : cluster_pt (f x) (map f F)⟩ :=
-      hs (calc map f F ≤ map f (𝓟 s) : map_mono F_le
-                  ... = 𝓟 (f '' s) : map_principal),
-    use [x, x_in],
-    suffices : (map f (𝓝 x ⊓ F)).ne_bot, by simpa [filter.map_ne_bot_iff],
-    rwa calc map f (𝓝 x ⊓ F) = map f ((comap f $ 𝓝 $ f x) ⊓ F) : by rw hf.nhds_eq_comap
-                          ... = 𝓝 (f x) ⊓ map f F : filter.push_pull' _ _ _ },
-  { intro hs,
-    exact hs.image hf.continuous }
-end
-
 /-- Finite topological spaces are compact. -/
 @[priority 100] instance fintype.compact_space [fintype α] : compact_space α :=
 { compact_univ := finite_univ.is_compact }
@@ -961,6 +957,37 @@ begin
   { exact λ _, is_open_interior }
 end
 
+protected lemma closed_embedding.locally_compact_space [locally_compact_space β] {f : α → β}
+  (hf : closed_embedding f) : locally_compact_space α :=
+begin
+  have : ∀ x : α, (𝓝 x).has_basis (λ s, s ∈ 𝓝 (f x) ∧ is_compact s) (λ s, f ⁻¹' s),
+  { intro x,
+    rw hf.to_embedding.to_inducing.nhds_eq_comap,
+    exact (compact_basis_nhds _).comap _ },
+  exact locally_compact_space_of_has_basis this (λ x s hs, hf.is_compact_preimage hs.2)
+end
+
+protected lemma is_closed.locally_compact_space [locally_compact_space α] {s : set α}
+  (hs : is_closed s) : locally_compact_space s :=
+(closed_embedding_subtype_coe hs).locally_compact_space
+
+protected lemma open_embedding.locally_compact_space [locally_compact_space β] {f : α → β}
+  (hf : open_embedding f) : locally_compact_space α :=
+begin
+  have : ∀ x : α, (𝓝 x).has_basis (λ s, (s ∈ 𝓝 (f x) ∧ is_compact s) ∧ s ⊆ range f) (λ s, f ⁻¹' s),
+  { intro x,
+    rw hf.to_embedding.to_inducing.nhds_eq_comap,
+    exact ((compact_basis_nhds _).restrict_subset $
+      hf.open_range.mem_nhds $ mem_range_self _).comap _ },
+  refine locally_compact_space_of_has_basis this (λ x s hs, _),
+  rw [← hf.to_inducing.is_compact_iff, image_preimage_eq_of_subset hs.2],
+  exact hs.1.2
+end
+
+protected lemma is_open.locally_compact_space [locally_compact_space α] {s : set α}
+  (hs : is_open s) : locally_compact_space s :=
+hs.open_embedding_subtype_coe.locally_compact_space
+
 lemma ultrafilter.le_nhds_Lim [compact_space α] (F : ultrafilter α) :
   ↑F ≤ 𝓝 (@Lim _ _ (F : filter α).nonempty_of_ne_bot F) :=
 begin
@@ -1061,7 +1088,7 @@ Union_eq_univ_iff.mp (Union_compact_covering α) x
 
 /-- If `α` is a `σ`-compact space, then a locally finite family of nonempty sets of `α` can have
 only countably many elements, `set.countable` version. -/
-lemma locally_finite.countable_of_sigma_compact {ι : Type*} {f : ι → set α} (hf : locally_finite f)
+protected lemma locally_finite.countable_univ {ι : Type*} {f : ι → set α} (hf : locally_finite f)
   (hne : ∀ i, (f i).nonempty) :
   countable (univ : set ι) :=
 begin
@@ -1072,6 +1099,12 @@ begin
   exact mem_Union.2 ⟨n, x, hx, hn⟩
 end
 
+/-- If `f : ι → set α` is a locally finite covering of a σ-compact topological space by nonempty
+sets, then the index type `ι` is encodable. -/
+protected noncomputable def locally_finite.encodable {ι : Type*} {f : ι → set α}
+  (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : encodable ι :=
+@encodable.of_equiv _ _ (hf.countable_univ hne).to_encodable (equiv.set.univ _).symm
+
 /-- In a topological space with sigma compact topology, if `f` is a function that sends each point
 `x` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`,
 the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`. -/