feat(topology/algebra/group): Addition of interiors (#10659)

This proves `interior s * t ⊆ interior (s * t)`, a few prerequisites, and generalizes to `is_open.mul_left`/`is_open.mul_right`.

Author: YaelDillies

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

@@ -682,7 +682,7 @@ begin
 end
 
 theorem ssubset_insert {s : set α} {a : α} (h : a ∉ s) : s ⊂ insert a s :=
-ssubset_iff_insert.2 ⟨a, h, subset.refl _⟩
+ssubset_iff_insert.2 ⟨a, h, subset.rfl⟩
 
 theorem insert_comm (a b : α) (s : set α) : insert a (insert b s) = insert b (insert a s) :=
 ext $ λ x, or.left_comm
@@ -1477,9 +1477,8 @@ instance (f : α → β) (s : set α) [nonempty s] : nonempty (f '' s) :=
   f '' s ⊆ t ↔ s ⊆ f ⁻¹' t :=
 ball_image_iff
 
-theorem image_preimage_subset (f : α → β) (s : set β) :
-  f '' (f ⁻¹' s) ⊆ s :=
-image_subset_iff.2 (subset.refl _)
+theorem image_preimage_subset (f : α → β) (s : set β) : f '' (f ⁻¹' s) ⊆ s :=
+image_subset_iff.2 subset.rfl
 
 theorem subset_preimage_image (f : α → β) (s : set α) :
   s ⊆ f ⁻¹' (f '' s) :=
@@ -2551,8 +2550,7 @@ variable {α : Type*}
 def inclusion {s t : set α} (h : s ⊆ t) : s → t :=
 λ x : s, (⟨x, h x.2⟩ : t)
 
-@[simp] lemma inclusion_self {s : set α} (x : s) :
-  inclusion (set.subset.refl _) x = x :=
+@[simp] lemma inclusion_self {s : set α} (x : s) : inclusion subset.rfl x = x :=
 by { cases x, refl }
 
 @[simp] lemma inclusion_right {s t : set α} (h : s ⊆ t) (x : t) (m : (x : α) ∈ s) :
@@ -2657,6 +2655,11 @@ 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.rfl ht
+
+lemma image2_subset_right (hs : s ⊆ s') : image2 f s t ⊆ image2 f s' t :=
+image2_subset hs subset.rfl
+
 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,13 @@ 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⁻¹ := hs.preimage continuous_inv
+
+@[to_additive]
+lemma is_closed.inv {s : set G} (hs : is_closed s) : is_closed s⁻¹ := hs.preimage continuous_inv
 
 namespace subgroup
 
@@ -566,27 +610,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 :=