feat(topology/bases): disjoint unions of second-countable spaces are …

…second-countable (#12061)

src/topology/bases.lean

@@ -107,9 +107,9 @@ end
 /-- A set `s` is in the neighbourhood of `a` iff there is some basis set `t`, which
 contains `a` and is itself contained in `s`. -/
 lemma is_topological_basis.mem_nhds_iff {a : α} {s : set α} {b : set (set α)}
-  (hb : is_topological_basis b) : s ∈ 𝓝 a ↔ ∃t∈b, a ∈ t ∧ t ⊆ s :=
+  (hb : is_topological_basis b) : s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s :=
 begin
-  change s ∈ (𝓝 a).sets ↔ ∃t∈b, a ∈ t ∧ t ⊆ s,
+  change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s,
   rw [hb.eq_generate_from, nhds_generate_from, binfi_sets_eq],
   { simp [and_assoc, and.left_comm] },
   { exact assume s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩,
@@ -121,6 +121,10 @@ begin
     exact ⟨i, h2, h1⟩ }
 end
 
+lemma is_topological_basis.is_open_iff {s : set α} {b : set (set α)} (hb : is_topological_basis b) :
+  is_open s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s :=
+by simp [is_open_iff_mem_nhds, hb.mem_nhds_iff]
+
 lemma is_topological_basis.nhds_has_basis {b : set (set α)} (hb : is_topological_basis b) {a : α} :
   (𝓝 a).has_basis (λ t : set α, t ∈ b ∧ a ∈ t) (λ t, t) :=
 ⟨λ s, hb.mem_nhds_iff.trans $ by simp only [exists_prop, and_assoc]⟩
@@ -367,6 +371,11 @@ begin
     refl }
 end
 
+lemma is_topological_basis_singletons (α : Type*) [topological_space α] [discrete_topology α] :
+  is_topological_basis {s | ∃ (x : α), (s : set α) = {x}} :=
+is_topological_basis_of_open_of_nhds (λ u hu, is_open_discrete _) $
+  λ x u hx u_open, ⟨{x}, ⟨x, rfl⟩, mem_singleton x, singleton_subset_iff.2 hx⟩
+
 /-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is
 a separable space as well. E.g., the completion of a separable uniform space is separable. -/
 protected lemma dense_range.separable_space {α β : Type*} [topological_space α] [separable_space α]
@@ -630,6 +639,88 @@ begin
   exact htU ⟨x, hx⟩
 end
 
+section sigma
+
+variables {ι : Type*} {E : ι → Type*} [∀ i, topological_space (E i)]
+omit t
+
+/-- In a disjoint union space `Σ i, E i`, one can form a topological basis by taking the union of
+topological bases on each of the parts of the space. -/
+lemma is_topological_basis.sigma
+  {s : Π (i : ι), set (set (E i))} (hs : ∀ i, is_topological_basis (s i)) :
+  is_topological_basis (⋃ (i : ι), (λ u, ((sigma.mk i) '' u : set (Σ i, E i))) '' (s i)) :=
+begin
+  apply is_topological_basis_of_open_of_nhds,
+  { assume u hu,
+    obtain ⟨i, t, ts, rfl⟩ : ∃ (i : ι) (t : set (E i)), t ∈ s i ∧ sigma.mk i '' t = u,
+      by simpa only [mem_Union, mem_image] using hu,
+    exact is_open_map_sigma_mk _ ((hs i).is_open ts) },
+  { rintros ⟨i, x⟩ u hxu u_open,
+    have hx : x ∈ sigma.mk i ⁻¹' u := hxu,
+    obtain ⟨v, vs, xv, hv⟩ : ∃ (v : set (E i)) (H : v ∈ s i), x ∈ v ∧ v ⊆ sigma.mk i ⁻¹' u :=
+      (hs i).exists_subset_of_mem_open hx (is_open_sigma_iff.1 u_open i),
+    exact ⟨(sigma.mk i) '' v, mem_Union.2 ⟨i, mem_image_of_mem _ vs⟩, mem_image_of_mem _ xv,
+      image_subset_iff.2 hv⟩ }
+end
+
+/-- A countable disjoint union of second countable spaces is second countable. -/
+instance [encodable ι] [∀ i, second_countable_topology (E i)] :
+  second_countable_topology (Σ i, E i) :=
+begin
+  let b := (⋃ (i : ι), (λ u, ((sigma.mk i) '' u : set (Σ i, E i))) '' (countable_basis (E i))),
+  have A : is_topological_basis b := is_topological_basis.sigma (λ i, is_basis_countable_basis  _),
+  have B : countable b := countable_Union (λ i, countable.image (countable_countable_basis _) _),
+  exact A.second_countable_topology B,
+end
+
+end sigma
+
+
+section sum
+omit t
+
+variables {β : Type*} [topological_space α] [topological_space β]
+
+/-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of
+topological bases on each of the two components. -/
+lemma is_topological_basis.sum
+  {s : set (set α)} (hs : is_topological_basis s) {t : set (set β)} (ht : is_topological_basis t) :
+  is_topological_basis (((λ u, sum.inl '' u) '' s) ∪ ((λ u, sum.inr '' u) '' t)) :=
+begin
+  apply is_topological_basis_of_open_of_nhds,
+  { assume u hu,
+    cases hu,
+    { rcases hu with ⟨w, hw, rfl⟩,
+      exact open_embedding_inl.is_open_map w (hs.is_open hw) },
+    { rcases hu with ⟨w, hw, rfl⟩,
+      exact open_embedding_inr.is_open_map w (ht.is_open hw) } },
+  { rintros x u hxu u_open,
+    cases x,
+    { have h'x : x ∈ sum.inl ⁻¹' u := hxu,
+      obtain ⟨v, vs, xv, vu⟩ : ∃ (v : set α) (H : v ∈ s), x ∈ v ∧ v ⊆ sum.inl ⁻¹' u :=
+        hs.exists_subset_of_mem_open h'x (is_open_sum_iff.1 u_open).1,
+      exact ⟨sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
+        image_subset_iff.2 vu⟩ },
+    { have h'x : x ∈ sum.inr ⁻¹' u := hxu,
+      obtain ⟨v, vs, xv, vu⟩ : ∃ (v : set β) (H : v ∈ t), x ∈ v ∧ v ⊆ sum.inr ⁻¹' u :=
+        ht.exists_subset_of_mem_open h'x (is_open_sum_iff.1 u_open).2,
+      exact ⟨sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
+        image_subset_iff.2 vu⟩ } }
+end
+
+/-- A sum type of two second countable spaces is second countable. -/
+instance [second_countable_topology α] [second_countable_topology β] :
+  second_countable_topology (α ⊕ β) :=
+begin
+  let b := (λ u, sum.inl '' u) '' (countable_basis α) ∪ (λ u, sum.inr '' u) '' (countable_basis β),
+  have A : is_topological_basis b := (is_basis_countable_basis α).sum (is_basis_countable_basis β),
+  have B : countable b := (countable.image (countable_countable_basis _) _).union
+    (countable.image (countable_countable_basis _) _),
+  exact A.second_countable_topology B,
+end
+
+end sum
+
 end topological_space
 
 open topological_space

src/topology/constructions.lean

@@ -642,6 +642,12 @@ is_open_sum_iff.2 $ by simp
 lemma is_open_range_inr : is_open (range (inr : β → α ⊕ β)) :=
 is_open_sum_iff.2 $ by simp
 
+lemma is_closed_range_inl : is_closed (range (inl : α → α ⊕ β)) :=
+by { rw [← is_open_compl_iff, compl_range_inl], exact is_open_range_inr }
+
+lemma is_closed_range_inr : is_closed (range (inr : β → α ⊕ β)) :=
+by { rw [← is_open_compl_iff, compl_range_inr], exact is_open_range_inl }
+
 lemma open_embedding_inl : open_embedding (inl : α → α ⊕ β) :=
 { open_range := is_open_range_inl,
   .. embedding_inl }
@@ -650,6 +656,14 @@ lemma open_embedding_inr : open_embedding (inr : β → α ⊕ β) :=
 { open_range := is_open_range_inr,
   .. embedding_inr }
 
+lemma closed_embedding_inl : closed_embedding (inl : α → α ⊕ β) :=
+{ closed_range := is_closed_range_inl,
+  .. embedding_inl }
+
+lemma closed_embedding_inr : closed_embedding (inr : β → α ⊕ β) :=
+{ closed_range := is_closed_range_inr,
+  .. embedding_inr }
+
 end sum
 
 section subtype

src/topology/continuous_on.lean

@@ -501,6 +501,29 @@ have ∀ t, is_open (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_open u ∧
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous_def]; simp only [this]
 
+/-- If a function is continuous on a set for some topologies, then it is
+continuous on the same set with respect to any finer topology on the source space. -/
+lemma continuous_on.mono_dom {α β : Type*} {t₁ t₂ : topological_space α} {t₃ : topological_space β}
+  (h₁ : t₂ ≤ t₁) {s : set α} {f : α → β} (h₂ : @continuous_on α β t₁ t₃ f s) :
+  @continuous_on α β t₂ t₃ f s :=
+begin
+  rw continuous_on_iff' at h₂ ⊢,
+  assume t ht,
+  rcases h₂ t ht with ⟨u, hu, h'u⟩,
+  exact ⟨u, h₁ u hu, h'u⟩
+end
+
+/-- If a function is continuous on a set for some topologies, then it is
+continuous on the same set with respect to any coarser topology on the target space. -/
+lemma continuous_on.mono_rng {α β : Type*} {t₁ : topological_space α} {t₂ t₃ : topological_space β}
+  (h₁ : t₂ ≤ t₃) {s : set α} {f : α → β} (h₂ : @continuous_on α β t₁ t₂ f s) :
+  @continuous_on α β t₁ t₃ f s :=
+begin
+  rw continuous_on_iff' at h₂ ⊢,
+  assume t ht,
+  exact h₂ t (h₁ t ht)
+end
+
 theorem continuous_on_iff_is_closed {f : α → β} {s : set α} :
   continuous_on f s ↔ ∀ t : set β, is_closed t → ∃ u, is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s :=
 have ∀ t, is_closed (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s,

src/topology/homeomorph.lean

@@ -441,6 +441,14 @@ def image (e : α ≃ₜ β) (s : set α) : s ≃ₜ e '' s :=
 
 end homeomorph
 
+/-- An inducing equiv between topological spaces is a homeomorphism. -/
+@[simps] def equiv.to_homeomorph_of_inducing [topological_space α] [topological_space β] (f : α ≃ β)
+  (hf : inducing f) :
+  α ≃ₜ β :=
+{ continuous_to_fun := hf.continuous,
+  continuous_inv_fun := hf.continuous_iff.2 $ by simpa using continuous_id,
+  .. f }
+
 namespace continuous
 variables [topological_space α] [topological_space β]
 

src/topology/order.lean

@@ -701,6 +701,13 @@ continuous_iff_le_induced.2 $ bot_le
 @[continuity] lemma continuous_top {t : tspace α} : cont t ⊤ f :=
 continuous_iff_coinduced_le.2 $ le_top
 
+lemma continuous_id_of_le {t t' : tspace α} (h : t ≤ t') : cont t t' id :=
+begin
+  rw continuous_def,
+  assume u hu,
+  exact h u hu
+end
+
 /- 𝓝 in the induced topology -/
 
 theorem mem_nhds_induced [T : topological_space α] (f : β → α) (a : β) (s : set β) :