feat(topology): continuous_pi_iff pi.has_continuous_mul pi.topologica…

…l_group (#6689)
leanprover-community · Mar 20, 2021 · 26fcfbc · 26fcfbc
1 parent 07282da
commit 26fcfbc
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 0 deletions.
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
@@ -179,6 +179,11 @@ instance [topological_space H] [group H] [topological_group H] :
   topological_group (G × H) :=
 { continuous_inv := continuous_inv.prod_map continuous_inv }
 
+@[to_additive]
+instance pi.topological_group {C : β → Type*} [∀ b, topological_space (C b)]
+  [∀ b, group (C b)] [∀ b, topological_group (C b)] : topological_group (Π b, C b) :=
+{ continuous_inv := continuous_pi (λ i, (continuous_apply i).inv) }
+
 variable (G)
 
 /-- Inversion in a topological group as a homeomorphism. -/

diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean
@@ -102,6 +102,12 @@ instance [topological_space N] [has_mul N] [has_continuous_mul N] : has_continuo
 ⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prod_mk
  ((continuous_snd.comp continuous_fst).mul (continuous_snd.comp continuous_snd))⟩
 
+@[to_additive]
+instance pi.has_continuous_mul {C : β → Type*} [∀ b, topological_space (C b)]
+  [∀ b, has_mul (C b)] [∀ b, has_continuous_mul (C b)] : has_continuous_mul (Π b, C b) :=
+{ continuous_mul := continuous_pi (λ i, continuous.mul
+    ((continuous_apply i).comp continuous_fst) ((continuous_apply i).comp continuous_snd)) }
+
 @[priority 100, to_additive]
 instance has_continuous_mul_of_discrete_topology [topological_space N]
   [has_mul N] [discrete_topology N] : has_continuous_mul N :=

diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
@@ -641,6 +641,10 @@ lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :
   continuous (λp:Πi, π i, p i) :=
 continuous_infi_dom continuous_induced_dom
 
+lemma continuous_pi_iff [topological_space α] [∀ i, topological_space (π i)] {f : α → Π i, π i} :
+  continuous f ↔ ∀ i, continuous (λ y, f y i) :=
+iff.intro (λ h i, (continuous_apply i).comp h) continuous_pi
+
 /-- Embedding a factor into a product space (by fixing arbitrarily all the other coordinates) is
 continuous. -/
 @[continuity]