feat(algebra/pointwise): more lemmas about pointwise actions (#9226)

This:
* Primes the existing lemmas about `group_with_zero` and adds their group counterparts
* Adds:
  * `smul_mem_smul_set_iff`
  * `set_smul_subset_set_smul_iff`
  * `set_smul_subset_iff`
  * `subset_set_smul_iff`
* Generalizes `zero_smul_set` to take weaker typeclasses

Author: eric-wieser

src/algebra/pointwise.lean

@@ -599,27 +599,71 @@ section
 
 variables {α : Type*} {β : Type*}
 
-/-- A nonempty set in a module is scaled by zero to the singleton
-containing 0 in the module. -/
-lemma zero_smul_set [semiring α] [add_comm_monoid β] [module α β] {s : set β} (h : s.nonempty) :
+/-- A nonempty set is scaled by zero to the singleton set containing 0. -/
+lemma zero_smul_set [has_zero α] [has_zero β] [smul_with_zero α β] {s : set β} (h : s.nonempty) :
   (0 : α) • s = (0 : set β) :=
 by simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]
 
-lemma mem_inv_smul_set_iff [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β)
-  (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A :=
-by simp only [← image_smul, mem_image, inv_smul_eq_iff' ha, exists_eq_right]
+section group
+variables [group α] [mul_action α β]
 
-lemma mem_smul_set_iff_inv_smul_mem [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0)
-  (A : set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
-by rw [← mem_inv_smul_set_iff $ inv_ne_zero ha, inv_inv']
+@[simp] lemma smul_mem_smul_set_iff {a : α} {A : set β} {x : β} : a • x ∈ a • A ↔ x ∈ A :=
+⟨λ h, begin
+  rw [←inv_smul_smul a x, ←inv_smul_smul a A],
+  exact smul_mem_smul_set h,
+end, smul_mem_smul_set⟩
 
-lemma preimage_smul [group α] [mul_action α β] (a : α) (t : set β) : (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
+lemma mem_smul_set_iff_inv_smul_mem {a : α} {A : set β} {x : β} : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
+show x ∈ mul_action.to_perm a '' A ↔ _, from mem_image_equiv
+
+lemma mem_inv_smul_set_iff {a : α} {A : set β} {x : β} : x ∈ a⁻¹ • A ↔ a • x ∈ A :=
+by simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]
+
+lemma preimage_smul (a : α) (t : set β) : (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
 ((mul_action.to_perm a).symm.image_eq_preimage _).symm
 
-lemma preimage_smul' [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) (t : set β) :
-  (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
+@[simp] lemma set_smul_subset_set_smul_iff {a : α} {A B : set β} : a • A ⊆ a • B ↔ A ⊆ B :=
+image_subset_image_iff $ mul_action.injective _
+
+lemma set_smul_subset_iff {a : α} {A B : set β} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B :=
+(image_subset_iff).trans $ iff_of_eq $ congr_arg _ $
+  preimage_equiv_eq_image_symm _ $ mul_action.to_perm _
+
+lemma subset_set_smul_iff {a : α} {A B : set β} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B :=
+iff.symm $ (image_subset_iff).trans $ iff.symm $ iff_of_eq $ congr_arg _ $
+  image_equiv_eq_preimage_symm _ $ mul_action.to_perm _
+
+end group
+
+section group_with_zero
+variables [group_with_zero α] [mul_action α β]
+
+@[simp] lemma smul_mem_smul_set_iff' {a : α} (ha : a ≠ 0) (A : set β)
+  (x : β) : a • x ∈ a • A ↔ x ∈ A :=
+show units.mk0 a ha • _ ∈ _ ↔ _, from smul_mem_smul_set_iff
+
+lemma mem_smul_set_iff_inv_smul_mem' {a : α} (ha : a ≠ 0) (A : set β) (x : β) :
+  x ∈ a • A ↔ a⁻¹ • x ∈ A :=
+show _ ∈ units.mk0 a ha • _ ↔ _, from mem_smul_set_iff_inv_smul_mem
+
+lemma mem_inv_smul_set_iff' {a : α} (ha : a ≠ 0) (A : set β) (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A :=
+show _ ∈ (units.mk0 a ha)⁻¹ • _ ↔ _, from mem_inv_smul_set_iff
+
+lemma preimage_smul' {a : α} (ha : a ≠ 0) (t : set β) : (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
 preimage_smul (units.mk0 a ha) t
 
+@[simp] lemma set_smul_subset_set_smul_iff' {a : α} (ha : a ≠ 0) {A B : set β} :
+  a • A ⊆ a • B ↔ A ⊆ B :=
+show units.mk0 a ha • _ ⊆ _ ↔ _, from set_smul_subset_set_smul_iff
+
+lemma set_smul_subset_iff' {a : α} (ha : a ≠ 0) {A B : set β} : a • A ⊆ B ↔ A ⊆ a⁻¹ • B :=
+show units.mk0 a ha • _ ⊆ _ ↔ _, from set_smul_subset_iff
+
+lemma subset_set_smul_iff' {a : α} (ha : a ≠ 0) {A B : set β} : A ⊆ a • B ↔ a⁻¹ • A ⊆ B :=
+show _ ⊆ units.mk0 a ha • _ ↔ _, from subset_set_smul_iff
+
+end group_with_zero
+
 end
 
 namespace finset

src/analysis/convex/basic.lean

@@ -809,7 +809,7 @@ lemma convex.mem_smul_of_zero_mem (h : convex 𝕜 s) {x : E} (zero_mem : (0 : E
   (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
   x ∈ t • s :=
 begin
-  rw mem_smul_set_iff_inv_smul_mem (zero_lt_one.trans_le ht).ne',
+  rw mem_smul_set_iff_inv_smul_mem' (zero_lt_one.trans_le ht).ne',
   exact h.smul_mem_of_zero_mem zero_mem hx ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one ht⟩,
 end
 

src/analysis/seminorm.lean

@@ -65,7 +65,7 @@ lemma balanced.absorbs_self (hA : balanced 𝕜 A) : absorbs 𝕜 A A :=
 begin
   use [1, zero_lt_one],
   intros a ha x hx,
-  rw mem_smul_set_iff_inv_smul_mem,
+  rw mem_smul_set_iff_inv_smul_mem',
   { apply hA a⁻¹,
     { rw norm_inv, exact inv_le_one ha },
     { rw mem_smul_set, use [x, hx] }},
@@ -130,7 +130,7 @@ begin
     rw [metric.mem_ball, dist_zero_right, norm_inv],
     calc ∥a∥⁻¹ ≤ r/2 : (inv_le (half_pos hr₁) ha₂).mp ha₁
     ...       < r : half_lt_self hr₁ },
-  rw [mem_smul_set_iff_inv_smul_mem (norm_pos_iff.mp ha₂)],
+  rw [mem_smul_set_iff_inv_smul_mem' (norm_pos_iff.mp ha₂)],
   exact hw₁ ha₃,
 end