feat(data/finset/pointwise): s • t is the union of the a • t (#14696

)

and a few other results leading to it. Also tag `set.coe_bUnion` with `norm_cast` and rename `finset.image_mul_prod`/`finset.add_image_prod` to `finset.image_mul_product`/`finset.image_add_product`

src/data/finset/basic.lean

@@ -2333,7 +2333,7 @@ protected def bUnion (s : finset α) (t : α → finset β) : finset β :=
 @[simp] lemma mem_bUnion {b : β} : b ∈ s.bUnion t ↔ ∃ a ∈ s, b ∈ t a :=
 by simp only [mem_def, bUnion_val, mem_dedup, mem_bind, exists_prop]
 
-@[simp] lemma coe_bUnion : (s.bUnion t : set β) = ⋃ x ∈ (s : set α), t x :=
+@[simp, norm_cast] lemma coe_bUnion : (s.bUnion t : set β) = ⋃ x ∈ (s : set α), t x :=
 by simp only [set.ext_iff, mem_bUnion, set.mem_Union, iff_self, mem_coe, implies_true_iff]
 
 @[simp] theorem bUnion_insert [decidable_eq α] {a : α} : (insert a s).bUnion t = t a ∪ s.bUnion t :=

src/data/finset/n_ary.lean

@@ -140,6 +140,12 @@ begin
     mem_insert_self _ _, ha⟩, h.trans $ image₂_subset (subset_insert _ _) $ subset_insert _ _⟩⟩,
 end
 
+lemma bUnion_image_left : s.bUnion (λ a, t.image $ f a) = image₂ f s t :=
+coe_injective $ by { push_cast, exact set.Union_image_left _ }
+
+lemma bUnion_image_right : t.bUnion (λ b, s.image $ λ a, f a b) = image₂ f s t :=
+coe_injective $ by { push_cast, exact set.Union_image_right _ }
+
 /-!
 ### Algebraic replacement rules
 

src/data/finset/pointwise.lean

@@ -153,8 +153,8 @@ localized "attribute [instance] finset.has_mul finset.has_add" in pointwise
 @[to_additive]
 lemma mul_def : s * t = (s.product t).image (λ p : α × α, p.1 * p.2) := rfl
 
-@[to_additive add_image_prod]
-lemma image_mul_prod : (s.product t).image (λ x : α × α, x.fst * x.snd)  = s * t := rfl
+@[to_additive]
+lemma image_mul_product : (s.product t).image (λ x : α × α, x.fst * x.snd) = s * t := rfl
 
 @[to_additive]
 lemma mem_mul {x : α} : x ∈ s * t ↔ ∃ y z, y ∈ s ∧ z ∈ t ∧ y * z = x := mem_image₂
@@ -717,6 +717,8 @@ subset_image₂
 
 end has_vsub
 
+open_locale pointwise
+
 /-! ### Translation/scaling of finsets -/
 
 section has_scalar
@@ -760,6 +762,9 @@ lemma smul_finset_singleton (b : β) : a • ({b} : finset β) = {a • b} := im
 @[to_additive] lemma smul_finset_inter_subset : a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ (a • s₂) :=
 image_inter_subset _ _ _
 
+@[simp] lemma bUnion_smul_finset (s : finset α) (t : finset β) : s.bUnion (• t) = s • t :=
+bUnion_image_left
+
 end has_scalar
 
 open_locale pointwise
@@ -857,4 +862,10 @@ instance no_zero_smul_divisors_finset [has_zero α] [has_zero β] [has_scalar α
 coe_injective.no_zero_smul_divisors _ coe_zero coe_smul_finset
 
 end instances
+
+lemma pairwise_disjoint_smul_iff [decidable_eq α] [left_cancel_semigroup α] {s : set α}
+  {t : finset α} :
+  s.pairwise_disjoint (• t) ↔ ((s : set α) ×ˢ (t : set α) : set (α × α)).inj_on (λ p, p.1 * p.2) :=
+by simp_rw [←pairwise_disjoint_coe, coe_smul_finset, set.pairwise_disjoint_smul_iff]
+
 end finset

src/data/set/lattice.lean

@@ -1347,6 +1347,12 @@ by { simp_rw [image2_subset_iff, mem_Inter], exact λ x hx y hy i j, mem_image2_
 lemma image2_eq_Union (s : set α) (t : set β) : image2 f s t = ⋃ (i ∈ s) (j ∈ t), {f i j} :=
 by simp_rw [←image_eq_Union, Union_image_left]
 
+lemma prod_eq_bUnion_left : s ×ˢ t = ⋃ a ∈ s, (λ b, (a, b)) '' t :=
+by rw [Union_image_left, image2_mk_eq_prod]
+
+lemma prod_eq_bUnion_right : s ×ˢ t = ⋃ b ∈ t, (λ a, (a, b)) '' s :=
+by rw [Union_image_right, image2_mk_eq_prod]
+
 end image2
 
 section seq

src/data/set/pairwise.lean

@@ -26,7 +26,7 @@ on `set.pairwise_disjoint`, even though the latter unfolds to something nicer.
 
 open set function
 
-variables {α ι ι' : Type*} {r p q : α → α → Prop}
+variables {α β γ ι ι' : Type*} {r p q : α → α → Prop}
 
 section pairwise
 variables {f g : ι → α} {s t u : set α} {a b : α}
@@ -385,6 +385,38 @@ noncomputable def bUnion_eq_sigma_of_disjoint {s : set ι} {f : ι → set α}
 (equiv.set_congr (bUnion_eq_Union _ _)).trans $ Union_eq_sigma_of_disjoint $
   λ ⟨i, hi⟩ ⟨j, hj⟩ ne, h hi hj $ λ eq, ne $ subtype.eq eq
 
+/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
+disjoint iff `f` is injective . -/
+lemma pairwise_disjoint_image_right_iff {f : α → β → γ} {s : set α} {t : set β}
+  (hf : ∀ a ∈ s, injective (f a)) :
+  s.pairwise_disjoint (λ a, f a '' t) ↔ (s ×ˢ t : set (α × β)).inj_on (λ p, f p.1 p.2) :=
+begin
+  refine ⟨λ hs x hx y hy (h : f _ _ = _), _, λ hs x hx y hy h, _⟩,
+  { suffices : x.1 = y.1,
+    { exact prod.ext this (hf _ hx.1 $ h.trans $ by rw this) },
+    refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, _⟩),
+    rw h,
+    exact mem_image_of_mem _ hy.2 },
+  { rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩,
+    exact h (congr_arg prod.fst $ hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab) }
+end
+
+/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
+disjoint iff `f` is injective . -/
+lemma pairwise_disjoint_image_left_iff {f : α → β → γ} {s : set α} {t : set β}
+  (hf : ∀ b ∈ t, injective (λ a, f a b)) :
+  t.pairwise_disjoint (λ b, (λ a, f a b) '' s) ↔ (s ×ˢ t : set (α × β)).inj_on (λ p, f p.1 p.2) :=
+begin
+  refine ⟨λ ht x hx y hy (h : f _ _ = _), _, λ ht x hx y hy h, _⟩,
+  { suffices : x.2 = y.2,
+    { exact prod.ext (hf _ hx.2 $ h.trans $ by rw this) this },
+    refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, _⟩),
+    rw h,
+    exact mem_image_of_mem _ hy.1 },
+  { rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩,
+    exact h (congr_arg prod.snd $ ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab) }
+end
+
 end set
 
 lemma pairwise_disjoint_fiber (f : ι → α) : pairwise (disjoint on (λ a : α, f ⁻¹' {a})) :=

src/data/set/pointwise.lean

@@ -863,6 +863,10 @@ image2_Inter₂_subset_right _ _ _
 
 @[to_additive] lemma finite.smul : s.finite → t.finite → (s • t).finite := finite.image2 _
 
+@[simp, to_additive] lemma bUnion_smul_set (s : set α) (t : set β) :
+  (⋃ a ∈ s, a • t) = s • t :=
+Union_image_left _
+
 end has_scalar
 
 section has_scalar_set
@@ -1174,6 +1178,15 @@ end
 
 end smul_with_zero
 
+section left_cancel_semigroup
+variables [left_cancel_semigroup α] {s t : set α}
+
+lemma pairwise_disjoint_smul_iff :
+  s.pairwise_disjoint (• t) ↔ (s ×ˢ t : set (α × α)).inj_on (λ p, p.1 * p.2) :=
+pairwise_disjoint_image_right_iff $ λ _ _, mul_right_injective _
+
+end left_cancel_semigroup
+
 section group
 variables [group α] [mul_action α β] {s t A B : set β} {a : α} {x : β}
 

src/data/set/prod.lean

@@ -253,6 +253,8 @@ set.ext $ λ a,
 ⟨ by { rintro ⟨_, _, rfl⟩, exact ⟨_, _, (mem_prod.mp ‹_›).1, (mem_prod.mp ‹_›).2, rfl⟩ },
   by { rintro ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), mem_prod.mpr ⟨‹_›, ‹_›⟩, rfl⟩ }⟩
 
+@[simp] lemma image2_mk_eq_prod : image2 prod.mk s t = s ×ˢ t := ext $ by simp
+
 end prod
 
 /-! ### Diagonal -/