feat(topology/connected): product of connected spaces is a connected …

…space (#9789)

* prove more in the RHS of `filter.mem_infi'`;
* prove that the product of (pre)connected sets is a (pre)connected set;
* prove a similar statement about indexed product `set.pi set.univ _`;
* add instances for `prod.preconnected_space`, `prod.connected_space`, `pi.preconnected_space`, and `pi.connected_space`.

src/order/filter/basic.lean

@@ -512,34 +512,28 @@ begin
 end
 
 lemma mem_infi' {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔
-  ∃ I : set ι, finite I ∧ ∃ V : ι → set α, (∀ i ∈ I, V i ∈ s i) ∧ U = ⋂ i ∈ I, V i  :=
+  ∃ I : set ι, finite I ∧ ∃ V : ι → set α, (∀ i, V i ∈ s i) ∧
+    (∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i :=
 begin
   simp only [mem_infi, set_coe.forall', bInter_eq_Inter],
-  refine ⟨_, λ ⟨I, If, V, hV⟩, ⟨I, If, λ i, V i, hV⟩⟩,
-  rintro ⟨I, If, V, hV⟩,
-  lift V to ι → set α using trivial,
-  exact ⟨I, If, V, hV⟩
+  refine ⟨_, λ ⟨I, If, V, hVs, _, hVU, _⟩, ⟨I, If, λ i, V i, λ i, hVs i, hVU⟩⟩,
+  rintro ⟨I, If, V, hV, rfl⟩,
+  refine ⟨I, If, λ i, if hi : i ∈ I then V ⟨i, hi⟩ else univ, λ i, _, λ i hi, _, _⟩,
+  { split_ifs, exacts [hV _, univ_mem] },
+  { exact dif_neg hi },
+  { simp [Inter_dite, bInter_eq_Inter] }
 end
 
 lemma exists_Inter_of_mem_infi {ι : Type*} {α : Type*} {f : ι → filter α} {s}
   (hs : s ∈ ⨅ i, f i) : ∃ t : ι → set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=
-begin
-  classical,
-  rcases mem_infi'.mp hs with ⟨I, I_fin, V, hV, rfl⟩,
-  refine ⟨λ i, if i ∈ I then V i else univ, _, _⟩,
-  { intro i,
-    split_ifs,
-    exacts [hV i h, univ_mem] },
-  { simp [Inter_ite] },
-end
+let ⟨I, If, V, hVs, hV', hVU, hVU'⟩ := mem_infi'.1 hs in ⟨V, hVs, hVU'⟩
 
 lemma mem_infi_of_fintype {ι : Type*} [fintype ι] {α : Type*} {f : ι → filter α} (s) :
   s ∈ (⨅ i, f i) ↔ ∃ t : ι → set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=
 begin
   refine ⟨exists_Inter_of_mem_infi, _⟩,
-  rw mem_infi',
-  rintros ⟨t, ht, ht'⟩,
-  exact ⟨univ, finite_univ, ⟨t, λ i _, ht i, by simp [ht']⟩⟩
+  rintro ⟨t, ht, rfl⟩,
+  exact Inter_mem.2 (λ i, mem_infi_of_mem i (ht i))
 end
 
 @[simp] lemma le_principal_iff {s : set α} {f : filter α} : f ≤ 𝓟 s ↔ s ∈ f :=
@@ -1489,11 +1483,7 @@ end
 
 @[simp] lemma frequently_comap {f : filter β} {φ : α → β} {P : α → Prop} :
   (∃ᶠ a in comap φ f, P a) ↔ ∃ᶠ b in f, ∃ a, φ a = b ∧ P a :=
-begin
-  classical,
-  erw [← not_iff_not, not_not, not_not, filter.eventually_comap],
-  simp only [not_exists, not_and],
-end
+by simp only [filter.frequently, eventually_comap, not_exists, not_and]
 
 end comap
 

src/topology/connected.lean

@@ -36,7 +36,7 @@ and in particular
 https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.
 -/
 
-open set classical topological_space
+open set function topological_space
 open_locale classical topological_space
 
 universes u v
@@ -72,6 +72,13 @@ is_preirreducible_empty.is_preconnected
 theorem is_connected_singleton {x} : is_connected ({x} : set α) :=
 is_irreducible_singleton.is_connected
 
+theorem is_preconnected_singleton {x} : is_preconnected ({x} : set α) :=
+is_connected_singleton.is_preconnected
+
+theorem set.subsingleton.is_preconnected {s : set α} (hs : s.subsingleton) :
+  is_preconnected s :=
+hs.induction_on is_preconnected_empty (λ x, is_preconnected_singleton)
+
 /-- If any point of a set is joined to a fixed point by a preconnected subset,
 then the original set is preconnected as well. -/
 theorem is_preconnected_of_forall {s : set α} (x : α)
@@ -92,10 +99,8 @@ theorem is_preconnected_of_forall_pair {s : set α}
   (H : ∀ x y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ is_preconnected t) :
   is_preconnected s :=
 begin
-  rintros u v hu hv hs ⟨x, xs, xu⟩ ⟨y, ys, yv⟩,
-  rcases H x y xs ys with ⟨t, ts, xt, yt, ht⟩,
-  have := ht u v hu hv(subset.trans ts hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩,
-  exact this.imp (λ z hz, ⟨ts hz.1, hz.2⟩)
+  rcases eq_empty_or_nonempty s with (rfl|⟨x, hx⟩),
+  exacts [is_preconnected_empty, is_preconnected_of_forall x (λ y, H x y hx)],
 end
 
 /-- A union of a family of preconnected sets with a common point is preconnected as well. -/
@@ -107,6 +112,11 @@ begin
   exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩
 end
 
+theorem is_preconnected_Union {ι : Sort*} {s : ι → set α} (h₁ : (⋂ i, s i).nonempty)
+  (h₂ : ∀ i, is_preconnected (s i)) :
+  is_preconnected (⋃ i, s i) :=
+exists.elim h₁ $ λ f hf, is_preconnected_sUnion f _ hf (forall_range_iff.2 h₂)
+
 theorem is_preconnected.union (x : α) {s t : set α} (H1 : x ∈ s) (H2 : x ∈ t)
   (H3 : is_preconnected s) (H4 : is_preconnected t) : is_preconnected (s ∪ t) :=
 sUnion_pair s t ▸ is_preconnected_sUnion x {s, t}
@@ -204,6 +214,60 @@ begin
   contradiction
 end⟩
 
+theorem is_preconnected.prod [topological_space β] {s : set α} {t : set β}
+  (hs : is_preconnected s) (ht : is_preconnected t) :
+  is_preconnected (s.prod t) :=
+begin
+  apply is_preconnected_of_forall_pair,
+  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha₁, hb₁⟩ ⟨ha₂, hb₂⟩,
+  refine ⟨prod.mk a₁ '' t ∪ flip prod.mk b₂ '' s, _,
+    or.inl ⟨b₁, hb₁, rfl⟩, or.inr ⟨a₂, ha₂, rfl⟩, _⟩,
+  { rintro _ (⟨y, hy, rfl⟩|⟨x, hx, rfl⟩),
+    exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩] },
+  { exact (ht.image _ (continuous.prod.mk _).continuous_on).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
+      ⟨a₁, ha₁, rfl⟩ (hs.image _ (continuous_id.prod_mk continuous_const).continuous_on) }
+end
+
+theorem is_connected.prod [topological_space β] {s : set α} {t : set β}
+  (hs : is_connected s) (ht : is_connected t) : is_connected (s.prod t) :=
+⟨hs.1.prod ht.1, hs.2.prod ht.2⟩
+
+theorem is_preconnected_univ_pi {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)]
+  {s : Π i, set (π i)} (hs : ∀ i, is_preconnected (s i)) :
+  is_preconnected (pi univ s) :=
+begin
+  rintros u v uo vo hsuv ⟨f, hfs, hfu⟩ ⟨g, hgs, hgv⟩,
+  rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩,
+  induction I using finset.induction_on with i I hi ihI,
+  { refine ⟨g, hgs, ⟨_, hgv⟩⟩, simpa using hI },
+  { rw [finset.piecewise_insert] at hI,
+    have := I.piecewise_mem_set_pi hfs hgs,
+    refine (hsuv this).elim ihI (λ h, _),
+    set S := update (I.piecewise f g) i '' (s i),
+    have hsub : S ⊆ pi univ s,
+    { refine image_subset_iff.2 (λ z hz, _),
+      rwa update_preimage_univ_pi,
+      exact λ j hj, this j trivial },
+    have hconn : is_preconnected S,
+      from (hs i).image _ (continuous_const.update i continuous_id).continuous_on,
+    have hSu : (S ∩ u).nonempty,
+      from ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩,
+    have hSv : (S ∩ v).nonempty,
+      from ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩,
+    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono _,
+    exact inter_subset_inter_left _ hsub }
+end
+
+@[simp] theorem is_connected_univ_pi {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)]
+  {s : Π i, set (π i)} :
+  is_connected (pi univ s) ↔ ∀ i, is_connected (s i) :=
+begin
+  simp only [is_connected, ← univ_pi_nonempty_iff, forall_and_distrib, and.congr_right_iff],
+  refine λ hne, ⟨λ hc i, _, is_preconnected_univ_pi⟩,
+  rw [← eval_image_univ_pi hne],
+  exact hc.image _ (continuous_apply _).continuous_on
+end
+
 /-- The connected component of a point is the maximal connected set
 that contains this point. -/
 def connected_component (x : α) : set α :=
@@ -296,6 +360,22 @@ begin
     exact ⟨⟨x⟩⟩ }
 end
 
+instance [topological_space β] [preconnected_space α] [preconnected_space β] :
+  preconnected_space (α × β) :=
+⟨by { rw ← univ_prod_univ, exact is_preconnected_univ.prod is_preconnected_univ }⟩
+
+instance [topological_space β] [connected_space α] [connected_space β] :
+  connected_space (α × β) :=
+⟨prod.nonempty⟩
+
+instance {ι : Type*} {π : ι → Type*} [∀ i, topological_space (π i)]
+  [∀ i, preconnected_space (π i)] : preconnected_space (Π i, π i) :=
+⟨by { rw ← pi_univ univ, exact is_preconnected_univ_pi (λ i, is_preconnected_univ) }⟩
+
+instance {ι : Type*} {π : ι → Type*} [∀ i, topological_space (π i)]
+  [∀ i, connected_space (π i)] : connected_space (Π i, π i) :=
+⟨classical.nonempty_pi.2 $ λ i, by apply_instance⟩
+
 @[priority 100] -- see Note [lower instance priority]
 instance preirreducible_space.preconnected_space (α : Type u) [topological_space α]
   [preirreducible_space α] : preconnected_space α :=
@@ -550,7 +630,7 @@ lemma preimage_connected_component_connected {β : Type*} [topological_space β]
 begin
   -- The following proof is essentially https://stacks.math.columbia.edu/tag/0377
   -- although the statement is slightly different
-  have hf : function.surjective f := function.surjective.of_comp (λ t : β, (connected_fibers t).1),
+  have hf : surjective f := surjective.of_comp (λ t : β, (connected_fibers t).1),
 
   split,
   { cases hf t with s hs,
@@ -730,7 +810,7 @@ lemma is_totally_disconnected_of_totally_disconnected_space [totally_disconnecte
 λ t hts ht, totally_disconnected_space.is_totally_disconnected_univ _ t.subset_univ ht
 
 lemma is_totally_disconnected_of_image [topological_space β] {f : α → β} (hf : continuous_on f s)
-  (hf' : function.injective f) (h : is_totally_disconnected (f '' s)) : is_totally_disconnected s :=
+  (hf' : injective f) (h : is_totally_disconnected (f '' s)) : is_totally_disconnected s :=
 λ t hts ht x x_in y y_in, hf' $ h _ (image_subset f hts) (ht.image f $ hf.mono hts)
   (mem_image_of_mem f x_in) (mem_image_of_mem f y_in)
 

src/topology/constructions.lean

@@ -788,6 +788,17 @@ lemma interior_pi_set [fintype ι] {α : ι → Type*} [Π i, topological_space
   interior (pi I s) = I.pi (λ i, interior (s i)) :=
 by { ext a, simp only [mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff] }
 
+lemma exists_finset_piecewise_mem_of_mem_nhds [decidable_eq ι] [Π i, topological_space (π i)]
+  {s : set (Π a, π a)} {x : Π a, π a} (hs : s ∈ 𝓝 x) (y : Π a, π a) :
+  ∃ I : finset ι, I.piecewise x y ∈ s :=
+begin
+  simp only [nhds_pi, mem_infi', mem_comap] at hs,
+  rcases hs with ⟨I, hI, V, hV, hV_univ, rfl, -⟩,
+  choose t ht htV using hV,
+  refine ⟨hI.to_finset, mem_bInter $ λ i hi, htV i _⟩,
+  simpa [hI.mem_to_finset.2 hi] using mem_of_mem_nhds (ht i)
+end
+
 lemma pi_eq_generate_from [∀a, topological_space (π a)] :
   Pi.topological_space =
   generate_from {g | ∃(s:Πa, set (π a)) (i : finset ι), (∀a∈i, is_open (s a)) ∧ g = pi ↑i s} :=

src/topology/continuous_on.lean

@@ -255,16 +255,16 @@ begin
   split,
   { haveI : Π i, inhabited (α i) := λ i, ⟨x i⟩,
     simp only [nhds_within, nhds_pi, inf_principal_eq_bot, mem_infi', mem_comap],
-    rintro ⟨I, hIf, V, hV, hVs⟩, choose! t htx htV using hV,
+    rintro ⟨I, hIf, V, hV, -, hVs, -⟩, choose! t htx htV using hV,
     contrapose! hVs,
     change ∀ i, ∃ᶠ y in 𝓝 (x i), y ∈ s i at hVs,
-    have : ∀ i ∈ I, (s i ∩ t i).nonempty, from λ i hi, ((hVs i).and_eventually (htx i hi)).exists,
-    choose! y hys hyt,
+    have : ∀ i, (s i ∩ t i).nonempty, from λ i, ((hVs i).and_eventually (htx i)).exists,
+    choose y hys hyt,
     choose z hzs using λ i, (hVs i).exists,
     suffices : I.piecewise y z ∈ (⋂ i ∈ I, V i) ∩ (pi univ s),
     { intro H, simpa [← H] },
-    refine ⟨mem_bInter $ λ i hi, htV i hi _, λ i hi', _⟩,
-    { simp only [mem_preimage, piecewise_eq_of_mem _ _ _ hi, hyt i hi] },
+    refine ⟨mem_bInter $ λ i hi, htV i _, λ i hi', _⟩,
+    { simp only [mem_preimage, piecewise_eq_of_mem _ _ _ hi, hyt i] },
     { by_cases hi : i ∈ I; simp * } },
   { rintro ⟨i, eq⟩,
     rw [← @map_eq_bot_iff _ _ _ (λ x : Π i, α i, x i)],