[Merged by Bors] - feat(topology/algebra/group): Addition of interiors

src/algebra/pointwise.lean

@@ -216,6 +216,12 @@ end
 lemma mul_subset_mul [has_mul α] (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ * s₂ ⊆ t₁ * t₂ :=
 image2_subset h₁ h₂
 
+@[to_additive]
+lemma mul_subset_mul_left [has_mul α] (h : t₁ ⊆ t₂) : s * t₁ ⊆ s * t₂ := image2_subset_left h
+
+@[to_additive]
+lemma mul_subset_mul_right [has_mul α] (h : s₁ ⊆ s₂) : s₁ * t ⊆ s₂ * t := image2_subset_right h
+
 lemma pow_subset_pow [monoid α] (hst : s ⊆ t) (n : ℕ) :
   s ^ n ⊆ t ^ n :=
 begin

src/data/set/basic.lean

@@ -2657,6 +2657,12 @@ lemma mem_image2_iff (hf : injective2 f) : f a b ∈ image2 f s t ↔ a ∈ s 
 lemma image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t' :=
 by { rintro _ ⟨a, b, ha, hb, rfl⟩, exact mem_image2_of_mem (hs ha) (ht hb) }
 
+lemma image2_subset_left (ht : t ⊆ t') : image2 f s t ⊆ image2 f s t' :=
+image2_subset (subset.refl _) ht
+
+lemma image2_subset_right (hs : s ⊆ s') : image2 f s t ⊆ image2 f s' t :=
+image2_subset hs $ subset.refl _
+
 lemma forall_image2_iff {p : γ → Prop} :
   (∀ z ∈ image2 f s t, p z) ↔ ∀ (x ∈ s) (y ∈ t), p (f x y) :=
 ⟨λ h x hx y hy, h _ ⟨x, y, hx, hy, rfl⟩, λ h z ⟨x, y, hx, hy, hz⟩, hz ▸ h x hx y hy⟩

src/topology/algebra/group.lean

@@ -3,9 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
-
-import order.filter.pointwise
 import group_theory.quotient_group
+import order.filter.pointwise
 import topology.algebra.monoid
 import topology.homeomorph
 import topology.compacts
@@ -119,6 +118,45 @@ lemma discrete_topology_iff_open_singleton_one : discrete_topology G ↔ is_open
 
 end continuous_mul_group
 
+/-!
+### Topological operations on pointwise sums and products
+
+A few results about interior and closure of the pointwise addition/multiplication of sets in groups
+with continuous addition/multiplication. See also `submonoid.top_closure_mul_self_eq` in
+`topology.algebra.monoid`.
+-/
+
+section pointwise
+variables [topological_space α] [group α] [has_continuous_mul α] {s t : set α}
+
+@[to_additive]
+lemma is_open.mul_left (ht : is_open t) :  is_open (s * t) :=
+begin
+  rw ←Union_mul_left_image,
+  exact is_open_Union (λ a, is_open_Union $ λ ha, is_open_map_mul_left a t ht),
+end
+
+@[to_additive]
+lemma is_open.mul_right (hs : is_open s) : is_open (s * t) :=
+begin
+  rw ←Union_mul_right_image,
+  exact is_open_Union (λ a, is_open_Union $ λ ha, is_open_map_mul_right a s hs),
+end
+
+@[to_additive]
+lemma subset_interior_mul_left : interior s * t ⊆ interior (s * t) :=
+interior_maximal (set.mul_subset_mul_right interior_subset) is_open_interior.mul_right
+
+@[to_additive]
+lemma subset_interior_mul_right : s * interior t ⊆ interior (s * t) :=
+interior_maximal (set.mul_subset_mul_left interior_subset) is_open_interior.mul_left
+
+@[to_additive]
+lemma subset_interior_mul : interior s * interior t ⊆ interior (s * t) :=
+(set.mul_subset_mul_left interior_subset).trans subset_interior_mul_left
+
+end pointwise
+
 section topological_group
 
 /-!
@@ -269,7 +307,15 @@ lemma homeomorph.shear_mul_right_symm_coe :
   ⇑(homeomorph.shear_mul_right G).symm = λ z : G × G, (z.1, z.1⁻¹ * z.2) :=
 rfl
 
-variable {G}
+variables {G}
+
+@[to_additive]
+lemma is_open.inv {s : set G} (hs : is_open s) : is_open s⁻¹ :=
+by { rw ←set.image_inv, exact (homeomorph.inv G).is_open_map _ hs }
+
+@[to_additive]
+lemma is_closed.inv {s : set G} (hs : is_closed s) : is_closed s⁻¹ :=
+by { rw ←set.image_inv, exact (homeomorph.inv G).is_closed_map _ hs }
 
 namespace subgroup
 
@@ -566,27 +612,7 @@ class add_group_with_zero_nhd (G : Type u) extends add_comm_group G :=
 section filter_mul
 
 section
-variables [topological_space G] [group G] [topological_group G]
-
-@[to_additive]
-lemma is_open.mul_left {s t : set G} : is_open t → is_open (s * t) := λ ht,
-begin
-  have : ∀a, is_open ((λ (x : G), a * x) '' t) :=
-    assume a, is_open_map_mul_left a t ht,
-  rw ← Union_mul_left_image,
-  exact is_open_Union (λa, is_open_Union $ λha, this _),
-end
-
-@[to_additive]
-lemma is_open.mul_right {s t : set G} : is_open s → is_open (s * t) := λ hs,
-begin
-  have : ∀a, is_open ((λ (x : G), x * a) '' s),
-    assume a, apply is_open_map_mul_right, exact hs,
-  rw ← Union_mul_right_image,
-  exact is_open_Union (λa, is_open_Union $ λha, this _),
-end
-
-variables (G)
+variables (G) [topological_space G] [group G] [topological_group G]
 
 @[to_additive]
 lemma topological_group.t1_space (h : @is_closed G _ {1}) : t1_space G :=