feat(data/local_equiv,topology/local_homeomorph): add local_equiv.pi and local_homeomorph.pi (#6574)

Author: urkud

src/data/equiv/local_equiv.lean

@@ -520,6 +520,29 @@ by ext x; simp [ext_iff]; tauto
 
 end prod
 
+section pi
+
+variables {ι : Type*} {αi βi : ι → Type*} (ei : Π i, local_equiv (αi i) (βi i))
+
+/-- The product of a family of local equivs, as a local equiv on the pi type. -/
+@[simps source target] protected def pi : local_equiv (Π i, αi i) (Π i, βi i) :=
+{ to_fun := λ f i, ei i (f i),
+  inv_fun := λ f i, (ei i).symm (f i),
+  source := pi univ (λ i, (ei i).source),
+  target := pi univ (λ i, (ei i).target),
+  map_source' := λ f hf i hi, (ei i).map_source (hf i hi),
+  map_target' := λ f hf i hi, (ei i).map_target (hf i hi),
+  left_inv' := λ f hf, funext $ λ i, (ei i).left_inv (hf i trivial),
+  right_inv' := λ f hf, funext $ λ i, (ei i).right_inv (hf i trivial) }
+
+attribute [mfld_simps] pi_source pi_target
+
+@[simp, mfld_simps] lemma pi_coe : ⇑(local_equiv.pi ei) = λ (f : Π i, αi i) i, ei i (f i) := rfl
+@[simp, mfld_simps] lemma pi_symm :
+  (local_equiv.pi ei).symm = local_equiv.pi (λ i, (ei i).symm) := rfl
+
+end pi
+
 end local_equiv
 
 namespace set

src/data/set/basic.lean

@@ -2146,6 +2146,17 @@ end
 lemma univ_pi_eq_empty_iff : pi univ t = ∅ ↔ ∃ i, t i = ∅ :=
 by simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]
 
+@[simp] lemma range_dcomp {β : ι → Type*} (f : Π i, α i → β i) :
+  range (λ (g : Π i, α i), (λ i, f i (g i))) = pi univ (λ i, range (f i)) :=
+begin
+  apply subset.antisymm,
+  { rintro _ ⟨x, rfl⟩ i -,
+    exact ⟨x i, rfl⟩ },
+  { intros x hx,
+    choose y hy using hx,
+    exact ⟨λ i, y i trivial, funext $ λ i, hy i trivial⟩ }
+end
+
 @[simp] lemma insert_pi (i : ι) (s : set ι) (t : Π i, set (α i)) :
   pi (insert i s) t = (eval i ⁻¹' t i) ∩ pi s t :=
 by { ext, simp [pi, or_imp_distrib, forall_and_distrib] }

src/topology/constructions.lean

@@ -213,7 +213,7 @@ hf.prod_mk_nhds hg
 lemma continuous_at.prod_map {f : α → γ} {g : β → δ} {p : α × β}
   (hf : continuous_at f p.fst) (hg : continuous_at g p.snd) :
   continuous_at (λ p : α × β, (f p.1, g p.2)) p :=
-(hf.comp continuous_fst.continuous_at).prod (hg.comp continuous_snd.continuous_at)
+(hf.comp continuous_at_fst).prod (hg.comp continuous_at_snd)
 
 lemma continuous_at.prod_map' {f : α → γ} {g : β → δ} {x : α} {y : β}
   (hf : continuous_at f x) (hg : continuous_at g y) :
@@ -663,6 +663,11 @@ lemma tendsto_pi [t : ∀i, topological_space (π i)] {f : α → Πi, π i} {g
   tendsto f u (𝓝 g) ↔ ∀ x, tendsto (λ i, f i x) u (𝓝 (g x)) :=
 by simp [nhds_pi, filter.tendsto_comap_iff]
 
+lemma continuous_at_pi [∀ i, topological_space (π i)] [topological_space α] {f : α → Π i, π i}
+  {x : α} :
+  continuous_at f x ↔ ∀ i, continuous_at (λ y, f y i) x :=
+tendsto_pi
+
 lemma is_open_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set (π a)}
   (hi : finite i) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) :=
 by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, (hs _ ha).preimage (continuous_apply _))

src/topology/continuous_on.lean

@@ -434,6 +434,16 @@ begin
   exact hf.prod_map hg,
 end
 
+lemma continuous_within_at_pi {ι : Type*} {π : ι → Type*} [∀ i, topological_space (π i)]
+  {f : α → Π i, π i} {s : set α} {x : α} :
+  continuous_within_at f s x ↔ ∀ i, continuous_within_at (λ y, f y i) s x :=
+tendsto_pi
+
+lemma continuous_on_pi {ι : Type*} {π : ι → Type*} [∀ i, topological_space (π i)]
+  {f : α → Π i, π i} {s : set α} :
+  continuous_on f s ↔ ∀ i, continuous_on (λ y, f y i) s :=
+⟨λ h i x hx, tendsto_pi.1 (h x hx) i, λ h x hx, tendsto_pi.2 (λ i, h i x hx)⟩
+
 theorem continuous_on_iff {f : α → β} {s : set α} :
   continuous_on f s ↔ ∀ x ∈ s, ∀ t : set β, is_open t → f x ∈ t → ∃ u, is_open u ∧ x ∈ u ∧
     u ∩ s ⊆ f ⁻¹' t :=

src/topology/local_homeomorph.lean

@@ -573,7 +573,7 @@ def prod (e : local_homeomorph α β) (e' : local_homeomorph γ δ) : local_home
   continuous_inv_fun := continuous_on.prod
     (e.continuous_inv_fun.comp continuous_fst.continuous_on (prod_subset_preimage_fst _ _))
     (e'.continuous_inv_fun.comp continuous_snd.continuous_on (prod_subset_preimage_snd _ _)),
-  ..e.to_local_equiv.prod e'.to_local_equiv }
+  to_local_equiv := e.to_local_equiv.prod e'.to_local_equiv }
 
 @[simp, mfld_simps] lemma prod_to_local_equiv (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
   (e.prod e').to_local_equiv = e.to_local_equiv.prod e'.to_local_equiv := rfl
@@ -604,6 +604,23 @@ local_homeomorph.eq_of_local_equiv_eq $
 
 end prod
 
+section pi
+
+variables {ι : Type*} [fintype ι] {Xi Yi : ι → Type*} [Π i, topological_space (Xi i)]
+  [Π i, topological_space (Yi i)] (ei : Π i, local_homeomorph (Xi i) (Yi i))
+
+/-- The product of a finite family of `local_homeomorph`s. -/
+@[simps to_local_equiv] def pi : local_homeomorph (Π i, Xi i) (Π i, Yi i) :=
+{ to_local_equiv := local_equiv.pi (λ i, (ei i).to_local_equiv),
+  open_source := is_open_set_pi finite_univ $ λ i hi, (ei i).open_source,
+  open_target := is_open_set_pi finite_univ $ λ i hi, (ei i).open_target,
+  continuous_to_fun := continuous_on_pi.2 $ λ i, (ei i).continuous_on.comp
+    (continuous_apply _).continuous_on (λ f hf, hf i trivial),
+  continuous_inv_fun := continuous_on_pi.2 $ λ i, (ei i).continuous_on_symm.comp
+    (continuous_apply _).continuous_on (λ f hf, hf i trivial) }
+
+end pi
+
 section continuity
 
 /-- Continuity within a set at a point can be read under right composition with a local