Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 5e526d1

Browse files
YaelDilliesYaelDillies
committed
feat(data/{set,finset}/pointwise): a • t ⊆ s • t (#18697)
Eta expansion in the lemma statements is deliberate, to make the left and right lemmas more similar and allow further rewrites. Also additivise `finset.bUnion_smul_finset`, fix the name of `finset.smul_finset_mem_smul_finset` to `finset.smul_mem_smul_finset`, move `image2_swap`/`image₂_swap` further up the file to let them be used in earlier proofs.
1 parent 210657c commit 5e526d1

5 files changed

Lines changed: 172 additions & 32 deletions

File tree

‎src/data/finset/n_ary.lean‎

Lines changed: 27 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ image₂_subset hs subset.rfl
7575
lemma image_subset_image₂_left (hb : b ∈ t) : s.image (λ a, f a b) ⊆ image₂ f s t :=
7676
image_subset_iff.2 $ λ a ha, mem_image₂_of_mem ha hb
7777

78-
lemma image_subset_image₂_right (ha : a ∈ s) : t.image (f a) ⊆ image₂ f s t :=
78+
lemma image_subset_image₂_right (ha : a ∈ s) : t.image (λ b, f a b) ⊆ image₂ f s t :=
7979
image_subset_iff.2 $ λ b, mem_image₂_of_mem ha
8080

8181
lemma forall_image₂_iff {p : γ → Prop} : (∀ z ∈ image₂ f s t, p z) ↔ ∀ (x ∈ s) (y ∈ t), p (f x y) :=
@@ -84,6 +84,12 @@ by simp_rw [←mem_coe, coe_image₂, forall_image2_iff]
8484
@[simp] lemma image₂_subset_iff : image₂ f s t ⊆ u ↔ ∀ (x ∈ s) (y ∈ t), f x y ∈ u :=
8585
forall_image₂_iff
8686

87+
lemma image₂_subset_iff_left : image₂ f s t ⊆ u ↔ ∀ a ∈ s, t.image (λ b, f a b) ⊆ u :=
88+
by simp_rw [image₂_subset_iff, image_subset_iff]
89+
90+
lemma image₂_subset_iff_right : image₂ f s t ⊆ u ↔ ∀ b ∈ t, s.image (λ a, f a b) ⊆ u :=
91+
by simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_swap α]
92+
8793
@[simp] lemma image₂_nonempty_iff : (image₂ f s t).nonempty ↔ s.nonempty ∧ t.nonempty :=
8894
by { rw [←coe_nonempty, coe_image₂], exact image2_nonempty_iff }
8995

@@ -113,6 +119,14 @@ coe_injective $ by { push_cast, exact image2_union_left }
113119
lemma image₂_union_right [decidable_eq β] : image₂ f s (t ∪ t') = image₂ f s t ∪ image₂ f s t' :=
114120
coe_injective $ by { push_cast, exact image2_union_right }
115121

122+
@[simp] lemma image₂_insert_left [decidable_eq α] :
123+
image₂ f (insert a s) t = t.image (λ b, f a b) ∪ image₂ f s t :=
124+
coe_injective $ by { push_cast, exact image2_insert_left }
125+
126+
@[simp] lemma image₂_insert_right [decidable_eq β] :
127+
image₂ f s (insert b t) = s.image (λ a, f a b) ∪ image₂ f s t :=
128+
coe_injective $ by { push_cast, exact image2_insert_right }
129+
116130
lemma image₂_inter_left [decidable_eq α] (hf : injective2 f) :
117131
image₂ f (s ∩ s') t = image₂ f s t ∩ image₂ f s' t :=
118132
coe_injective $ by { push_cast, exact image2_inter_left hf }
@@ -214,10 +228,6 @@ lemma image₂_image_right (f : α → γ → δ) (g : β → γ) :
214228
image₂ f s (t.image g) = image₂ (λ a b, f a (g b)) s t :=
215229
coe_injective $ by { push_cast, exact image2_image_right _ _ }
216230

217-
lemma image₂_swap (f : α → β → γ) (s : finset α) (t : finset β) :
218-
image₂ f s t = image₂ (λ a b, f b a) t s :=
219-
coe_injective $ by { push_cast, exact image2_swap _ _ _ }
220-
221231
@[simp] lemma image₂_mk_eq_product [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
222232
image₂ prod.mk s t = s ×ˢ t :=
223233
by ext; simp [prod.ext_iff]
@@ -229,6 +239,10 @@ by { classical, rw [←image₂_mk_eq_product, image_image₂, curry] }
229239
@[simp] lemma image_uncurry_product (f : α → β → γ) (s : finset α) (t : finset β) :
230240
(s ×ˢ t).image (uncurry f) = image₂ f s t := by rw [←image₂_curry, curry_uncurry]
231241

242+
lemma image₂_swap (f : α → β → γ) (s : finset α) (t : finset β) :
243+
image₂ f s t = image₂ (λ a b, f b a) t s :=
244+
coe_injective $ by { push_cast, exact image2_swap _ _ _ }
245+
232246
@[simp] lemma image₂_left [decidable_eq α] (h : t.nonempty) : image₂ (λ x y, x) s t = s :=
233247
coe_injective $ by { push_cast, exact image2_left h }
234248

@@ -346,6 +360,14 @@ by rw [image₂_singleton_right, funext h, image_id']
346360

347361
variables [decidable_eq α] [decidable_eq β]
348362

363+
lemma image₂_inter_union_subset_union :
364+
image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
365+
coe_subset.1 $ by { push_cast, exact set.image2_inter_union_subset_union }
366+
367+
lemma image₂_union_inter_subset_union :
368+
image₂ f (s ∪ s') (t ∩ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
369+
coe_subset.1 $ by { push_cast, exact set.image2_union_inter_subset_union }
370+
349371
lemma image₂_inter_union_subset {f : α → α → β} {s t : finset α} (hf : ∀ a b, f a b = f b a) :
350372
image₂ f (s ∩ t) (s ∪ t) ⊆ image₂ f s t :=
351373
coe_subset.1 $ by { push_cast, exact image2_inter_union_subset hf }

‎src/data/finset/pointwise.lean‎

Lines changed: 60 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ finset multiplication, finset addition, pointwise addition, pointwise multiplica
5454
pointwise subtraction
5555
-/
5656

57-
open function
57+
open function mul_opposite
5858
open_locale big_operators pointwise
5959

6060
variables {F α β γ : Type*}
@@ -124,7 +124,9 @@ localized "attribute [instance] finset.has_inv finset.has_neg" in pointwise
124124
@[simp, to_additive] lemma inv_empty : (∅ : finset α)⁻¹ = ∅ := image_empty _
125125
@[simp, to_additive] lemma inv_nonempty_iff : s⁻¹.nonempty ↔ s.nonempty := nonempty.image_iff _
126126

127-
alias inv_nonempty_iff ↔ nonempty.inv nonempty.of_inv
127+
alias inv_nonempty_iff ↔ nonempty.of_inv nonempty.inv
128+
129+
attribute [to_additive] nonempty.inv nonempty.of_inv
128130

129131
@[to_additive, mono] lemma inv_subset_inv (h : s ⊆ t) : s⁻¹ ⊆ t⁻¹ := image_subset_image h
130132

@@ -212,6 +214,10 @@ attribute [mono] add_subset_add
212214
image₂_inter_subset_left
213215
@[to_additive] lemma mul_inter_subset : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂) :=
214216
image₂_inter_subset_right
217+
@[to_additive] lemma inter_mul_union_subset_union : s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ (s₁ * t₁) ∪ (s₂ * t₂) :=
218+
image₂_inter_union_subset_union
219+
@[to_additive] lemma union_mul_inter_subset_union : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ (s₁ * t₁) ∪ (s₂ * t₂) :=
220+
image₂_union_inter_subset_union
215221

216222
/-- If a finset `u` is contained in the product of two sets `s * t`, we can find two finsets `s'`,
217223
`t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' * t'`. -/
@@ -294,6 +300,10 @@ attribute [mono] sub_subset_sub
294300
image₂_inter_subset_left
295301
@[to_additive] lemma div_inter_subset : s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂) :=
296302
image₂_inter_subset_right
303+
@[to_additive] lemma inter_div_union_subset_union : (s₁ ∩ s₂) / (t₁ ∪ t₂) ⊆ (s₁ / t₁) ∪ (s₂ / t₂) :=
304+
image₂_inter_union_subset_union
305+
@[to_additive] lemma union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ (s₁ / t₁) ∪ (s₂ / t₂) :=
306+
image₂_union_inter_subset_union
297307

298308
/-- If a finset `u` is contained in the product of two sets `s / t`, we can find two finsets `s'`,
299309
`t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' / t'`. -/
@@ -711,6 +721,12 @@ image₂_union_left
711721
image₂_inter_subset_left
712722
@[to_additive] lemma smul_inter_subset : s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂ :=
713723
image₂_inter_subset_right
724+
@[to_additive] lemma inter_smul_union_subset_union [decidable_eq α] :
725+
(s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ (s₁ • t₁) ∪ (s₂ • t₂) :=
726+
image₂_inter_union_subset_union
727+
@[to_additive] lemma union_smul_inter_subset_union [decidable_eq α] :
728+
(s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ (s₁ • t₁) ∪ (s₂ • t₂) :=
729+
image₂_union_inter_subset_union
714730

715731
/-- If a finset `u` is contained in the scalar product of two sets `s • t`, we can find two finsets
716732
`s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' • t'`. -/
@@ -806,7 +822,7 @@ by simp only [finset.smul_finset_def, and.assoc, mem_image, exists_prop, prod.ex
806822
@[simp, norm_cast, to_additive]
807823
lemma coe_smul_finset (a : α) (s : finset β) : (↑(a • s) : set β) = a • s := coe_image
808824

809-
@[to_additive] lemma smul_finset_mem_smul_finset : b ∈ s → a • b ∈ a • s := mem_image_of_mem _
825+
@[to_additive] lemma smul_mem_smul_finset : b ∈ s → a • b ∈ a • s := mem_image_of_mem _
810826
@[to_additive] lemma smul_finset_card_le : (a • s).card ≤ s.card := card_image_le
811827

812828
@[simp, to_additive] lemma smul_finset_empty (a : α) : a • (∅ : finset β) = ∅ := image_empty _
@@ -829,7 +845,11 @@ lemma smul_finset_singleton (b : β) : a • ({b} : finset β) = {a • b} := im
829845
@[to_additive] lemma smul_finset_inter_subset : a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ (a • s₂) :=
830846
image_inter_subset _ _ _
831847

832-
@[simp] lemma bUnion_smul_finset (s : finset α) (t : finset β) : s.bUnion (• t) = s • t :=
848+
@[to_additive] lemma smul_finset_subset_smul {s : finset α} : a ∈ s → a • t ⊆ s • t :=
849+
image_subset_image₂_right
850+
851+
@[simp, to_additive] lemma bUnion_smul_finset (s : finset α) (t : finset β) :
852+
s.bUnion (• t) = s • t :=
833853
bUnion_image_left
834854

835855
end has_smul
@@ -936,6 +956,42 @@ coe_injective.no_zero_smul_divisors _ coe_zero coe_smul_finset
936956

937957
end instances
938958

959+
section has_smul
960+
variables [decidable_eq β] [decidable_eq γ] [has_smul αᵐᵒᵖ β] [has_smul β γ] [has_smul α γ]
961+
962+
-- TODO: replace hypothesis and conclusion with a typeclass
963+
@[to_additive] lemma op_smul_finset_smul_eq_smul_smul_finset (a : α) (s : finset β) (t : finset γ)
964+
(h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) :
965+
(op a • s) • t = s • a • t :=
966+
by { ext, simp [mem_smul, mem_smul_finset, h] }
967+
968+
end has_smul
969+
970+
section has_mul
971+
variables [has_mul α] [decidable_eq α] {s t u : finset α} {a : α}
972+
973+
@[to_additive] lemma op_smul_finset_subset_mul : a ∈ t → op a • s ⊆ s * t :=
974+
image_subset_image₂_left
975+
976+
@[simp, to_additive] lemma bUnion_op_smul_finset (s t : finset α) :
977+
t.bUnion (λ a, op a • s) = s * t :=
978+
bUnion_image_right
979+
980+
@[to_additive] lemma mul_subset_iff_left : s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u := image₂_subset_iff_left
981+
@[to_additive] lemma mul_subset_iff_right : s * t ⊆ u ↔ ∀ b ∈ t, op b • s ⊆ u :=
982+
image₂_subset_iff_right
983+
984+
end has_mul
985+
986+
section semigroup
987+
variables [semigroup α] [decidable_eq α]
988+
989+
@[to_additive] lemma op_smul_finset_mul_eq_mul_smul_finset (a : α) (s : finset α) (t : finset α) :
990+
(op a • s) * t = s * a • t :=
991+
op_smul_finset_smul_eq_smul_smul_finset _ _ _ $ λ _ _ _, mul_assoc _ _ _
992+
993+
end semigroup
994+
939995
section left_cancel_semigroup
940996
variables [left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α)
941997

‎src/data/set/n_ary.lean‎

Lines changed: 28 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,12 @@ lemma forall_image2_iff {p : γ → Prop} :
6767
image2 f s t ⊆ u ↔ ∀ (x ∈ s) (y ∈ t), f x y ∈ u :=
6868
forall_image2_iff
6969

70+
lemma image2_subset_iff_left : image2 f s t ⊆ u ↔ ∀ a ∈ s, (λ b, f a b) '' t ⊆ u :=
71+
by simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]
72+
73+
lemma image2_subset_iff_right : image2 f s t ⊆ u ↔ ∀ b ∈ t, (λ a, f a b) '' s ⊆ u :=
74+
by simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_swap α]
75+
7076
variables (f)
7177

7278
@[simp] lemma image_prod : (λ x : α × β, f x.1 x.2) '' s ×ˢ t = image2 f s t :=
@@ -83,6 +89,9 @@ image_prod _
8389
image2 (λ a b, f (a, b)) s t = f '' s ×ˢ t :=
8490
by simp [←image_uncurry_prod, uncurry]
8591

92+
lemma image2_swap (s : set α) (t : set β) : image2 f s t = image2 (λ a b, f b a) t s :=
93+
by { ext, split; rintro ⟨a, b, ha, hb, rfl⟩; refine ⟨b, a, hb, ha, rfl⟩ }
94+
8695
variables {f}
8796

8897
lemma image2_union_left : image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t :=
@@ -95,13 +104,7 @@ begin
95104
end
96105

97106
lemma image2_union_right : image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t' :=
98-
begin
99-
ext c,
100-
split,
101-
{ rintro ⟨a, b, ha, h1b|h2b, rfl⟩;[left, right]; exact ⟨_, _, ‹_›, ‹_›, rfl⟩ },
102-
{ rintro (⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩); refine ⟨_, _, ‹_›, _, rfl⟩;
103-
simp [mem_union, *] }
104-
end
107+
by rw [←image2_swap, image2_union_left, image2_swap f, image2_swap f]
105108

106109
lemma image2_inter_left (hf : injective2 f) : image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t :=
107110
by simp_rw [←image_uncurry_prod, inter_prod, image_inter hf.uncurry]
@@ -138,6 +141,12 @@ by { rintro _ ⟨a, b, ha, ⟨h1b, h2b⟩, rfl⟩, split; exact ⟨_, _, ‹_›
138141

139142
lemma image2_singleton : image2 f {a} {b} = {f a b} := by simp
140143

144+
@[simp] lemma image2_insert_left : image2 f (insert a s) t = (λ b, f a b) '' t ∪ image2 f s t :=
145+
by rw [insert_eq, image2_union_left, image2_singleton_left]
146+
147+
@[simp] lemma image2_insert_right : image2 f s (insert b t) = (λ a, f a b) '' s ∪ image2 f s t :=
148+
by rw [insert_eq, image2_union_right, image2_singleton_right]
149+
141150
@[congr] lemma image2_congr (h : ∀ (a ∈ s) (b ∈ t), f a b = f' a b) :
142151
image2 f s t = image2 f' s t :=
143152
by { ext, split; rintro ⟨a, b, ha, hb, rfl⟩; refine ⟨a, b, ha, hb, by rw h a ha b hb⟩ }
@@ -208,10 +217,6 @@ begin
208217
{ rintro ⟨a, b, ha, hb, rfl⟩, refine ⟨a, _, ha, ⟨b, hb, rfl⟩, rfl⟩ }
209218
end
210219

211-
lemma image2_swap (f : α → β → γ) (s : set α) (t : set β) :
212-
image2 f s t = image2 (λ a b, f b a) t s :=
213-
by { ext, split; rintro ⟨a, b, ha, hb, rfl⟩; refine ⟨b, a, hb, ha, rfl⟩ }
214-
215220
@[simp] lemma image2_left (h : t.nonempty) : image2 (λ x y, x) s t = s :=
216221
by simp [nonempty_def.mp h, ext_iff]
217222

@@ -339,14 +344,20 @@ lemma image2_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b =
339344
image2 f s {b} = s :=
340345
by rw [image2_singleton_right, funext h, image_id']
341346

347+
lemma image2_inter_union_subset_union :
348+
image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t' :=
349+
by { rw image2_union_right, exact union_subset_union
350+
(image2_subset_right $ inter_subset_left _ _) (image2_subset_right $ inter_subset_right _ _) }
351+
352+
lemma image2_union_inter_subset_union :
353+
image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t' :=
354+
by { rw image2_union_left, exact union_subset_union
355+
(image2_subset_left $ inter_subset_left _ _) (image2_subset_left $ inter_subset_right _ _) }
356+
342357
lemma image2_inter_union_subset {f : α → α → β} {s t : set α} (hf : ∀ a b, f a b = f b a) :
343358
image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t :=
344-
begin
345-
rintro _ ⟨a, b, ha, hb | hb, rfl⟩,
346-
{ rw hf,
347-
exact mem_image2_of_mem hb ha.2 },
348-
{ exact mem_image2_of_mem ha.1 hb }
349-
end
359+
by { rw inter_comm,
360+
exact image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset subset.rfl) }
350361

351362
lemma image2_union_inter_subset {f : α → α → β} {s t : set α} (hf : ∀ a b, f a b = f b a) :
352363
image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t :=

‎src/data/set/pointwise/basic.lean‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -223,6 +223,10 @@ attribute [mono] add_subset_add
223223
image2_inter_subset_left
224224
@[to_additive] lemma mul_inter_subset : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂) :=
225225
image2_inter_subset_right
226+
@[to_additive] lemma inter_mul_union_subset_union : s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ (s₁ * t₁) ∪ (s₂ * t₂) :=
227+
image2_inter_union_subset_union
228+
@[to_additive] lemma union_mul_inter_subset_union : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ (s₁ * t₁) ∪ (s₂ * t₂) :=
229+
image2_union_inter_subset_union
226230

227231
@[to_additive] lemma Union_mul_left_image : (⋃ a ∈ s, ((*) a) '' t) = s * t := Union_image_left _
228232
@[to_additive] lemma Union_mul_right_image : (⋃ a ∈ t, (* a) '' s) = s * t := Union_image_right _
@@ -324,6 +328,10 @@ attribute [mono] sub_subset_sub
324328
image2_inter_subset_left
325329
@[to_additive] lemma div_inter_subset : s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂) :=
326330
image2_inter_subset_right
331+
@[to_additive] lemma inter_div_union_subset_union : s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ (s₁ / t₁) ∪ (s₂ / t₂) :=
332+
image2_inter_union_subset_union
333+
@[to_additive] lemma union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ (s₁ / t₁) ∪ (s₂ / t₂) :=
334+
image2_union_inter_subset_union
327335

328336
@[to_additive] lemma Union_div_left_image : (⋃ a ∈ s, ((/) a) '' t) = s / t := Union_image_left _
329337
@[to_additive] lemma Union_div_right_image : (⋃ a ∈ t, (/ a) '' s) = s / t := Union_image_right _
@@ -412,8 +420,8 @@ variables [mul_one_class α]
412420
/-- `set α` is a `mul_one_class` under pointwise operations if `α` is. -/
413421
@[to_additive "`set α` is an `add_zero_class` under pointwise operations if `α` is."]
414422
protected def mul_one_class : mul_one_class (set α) :=
415-
{ mul_one := λ s, by { simp only [← singleton_one, mul_singleton, mul_one, image_id'] },
416-
one_mul := λ s, by { simp only [← singleton_one, singleton_mul, one_mul, image_id'] },
423+
{ mul_one := image2_right_identity mul_one,
424+
one_mul := image2_left_identity one_mul,
417425
..set.has_one, ..set.has_mul }
418426

419427
localized "attribute [instance] set.mul_one_class set.add_zero_class set.semigroup set.add_semigroup

0 commit comments

Comments
 (0)