From d5d186a1c10fce0afec56557791b69d1e32546fa Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 30 Sep 2024 20:40:41 +0000 Subject: [PATCH] feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations (#17253) Provides `sInter` and `sUnion` versions of pointwise algebraic operations on sets. Needed in #17029 Co-authored-by: Christopher Hoskin --- .../Algebra/Group/Pointwise/Set/Basic.lean | 166 +++++++++++++----- Mathlib/Data/Set/Lattice.lean | 26 +++ 2 files changed, 147 insertions(+), 45 deletions(-) diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean index 1ab1dcd9ea7a1..df2bf0c9e4874 100644 --- a/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean +++ b/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean @@ -181,10 +181,18 @@ theorem union_inv : (s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹ := theorem iInter_inv (s : ι → Set α) : (⋂ i, s i)⁻¹ = ⋂ i, (s i)⁻¹ := preimage_iInter +@[to_additive (attr := simp)] +theorem sInter_inv (S : Set (Set α)) : (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹ := + preimage_sInter + @[to_additive (attr := simp)] theorem iUnion_inv (s : ι → Set α) : (⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹ := preimage_iUnion +@[to_additive (attr := simp)] +theorem sUnion_inv (S : Set (Set α)) : (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹ := + preimage_sUnion + @[to_additive (attr := simp)] theorem compl_inv : sᶜ⁻¹ = s⁻¹ᶜ := preimage_compl @@ -236,7 +244,7 @@ theorem inv_insert (a : α) (s : Set α) : (insert a s)⁻¹ = insert a⁻¹ s @[to_additive] theorem inv_range {ι : Sort*} {f : ι → α} : (range f)⁻¹ = range fun i => (f i)⁻¹ := by rw [← image_inv] - exact (range_comp _ _).symm + exact (range_comp ..).symm open MulOpposite @@ -374,47 +382,63 @@ theorem iUnion_mul_right_image : ⋃ a ∈ t, (· * a) '' s = s * t := @[to_additive] theorem iUnion_mul (s : ι → Set α) (t : Set α) : (⋃ i, s i) * t = ⋃ i, s i * t := - image2_iUnion_left _ _ _ + image2_iUnion_left .. @[to_additive] theorem mul_iUnion (s : Set α) (t : ι → Set α) : (s * ⋃ i, t i) = ⋃ i, s * t i := - image2_iUnion_right _ _ _ + image2_iUnion_right .. + +@[to_additive] +theorem sUnion_mul (S : Set (Set α)) (t : Set α) : ⋃₀ S * t = ⋃ s ∈ S, s * t := + image2_sUnion_left .. + +@[to_additive] +theorem mul_sUnion (s : Set α) (T : Set (Set α)) : s * ⋃₀ T = ⋃ t ∈ T, s * t := + image2_sUnion_right .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem iUnion₂_mul (s : ∀ i, κ i → Set α) (t : Set α) : (⋃ (i) (j), s i j) * t = ⋃ (i) (j), s i j * t := - image2_iUnion₂_left _ _ _ + image2_iUnion₂_left .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem mul_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) : (s * ⋃ (i) (j), t i j) = ⋃ (i) (j), s * t i j := - image2_iUnion₂_right _ _ _ + image2_iUnion₂_right .. @[to_additive] theorem iInter_mul_subset (s : ι → Set α) (t : Set α) : (⋂ i, s i) * t ⊆ ⋂ i, s i * t := - Set.image2_iInter_subset_left _ _ _ + Set.image2_iInter_subset_left .. @[to_additive] theorem mul_iInter_subset (s : Set α) (t : ι → Set α) : (s * ⋂ i, t i) ⊆ ⋂ i, s * t i := - image2_iInter_subset_right _ _ _ + image2_iInter_subset_right .. + +@[to_additive] +lemma mul_sInter_subset (s : Set α) (T : Set (Set α)) : + s * ⋂₀ T ⊆ ⋂ t ∈ T, s * t := image2_sInter_right_subset s T (fun a b => a * b) + +@[to_additive] +lemma sInter_mul_subset (S : Set (Set α)) (t : Set α) : + ⋂₀ S * t ⊆ ⋂ s ∈ S, s * t := image2_sInter_left_subset S t (fun a b => a * b) /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem iInter₂_mul_subset (s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) * t ⊆ ⋂ (i) (j), s i j * t := - image2_iInter₂_subset_left _ _ _ + image2_iInter₂_subset_left .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem mul_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set α) : (s * ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s * t i j := - image2_iInter₂_subset_right _ _ _ + image2_iInter₂_subset_right .. /-- The singleton operation as a `MulHom`. -/ @[to_additive "The singleton operation as an `AddHom`."] @@ -562,47 +586,63 @@ theorem iUnion_div_right_image : ⋃ a ∈ t, (· / a) '' s = s / t := @[to_additive] theorem iUnion_div (s : ι → Set α) (t : Set α) : (⋃ i, s i) / t = ⋃ i, s i / t := - image2_iUnion_left _ _ _ + image2_iUnion_left .. @[to_additive] theorem div_iUnion (s : Set α) (t : ι → Set α) : (s / ⋃ i, t i) = ⋃ i, s / t i := - image2_iUnion_right _ _ _ + image2_iUnion_right .. + +@[to_additive] +theorem sUnion_div (S : Set (Set α)) (t : Set α) : ⋃₀ S / t = ⋃ s ∈ S, s / t := + image2_sUnion_left .. + +@[to_additive] +theorem div_sUnion (s : Set α) (T : Set (Set α)) : s / ⋃₀ T = ⋃ t ∈ T, s / t := + image2_sUnion_right .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem iUnion₂_div (s : ∀ i, κ i → Set α) (t : Set α) : (⋃ (i) (j), s i j) / t = ⋃ (i) (j), s i j / t := - image2_iUnion₂_left _ _ _ + image2_iUnion₂_left .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem div_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) : (s / ⋃ (i) (j), t i j) = ⋃ (i) (j), s / t i j := - image2_iUnion₂_right _ _ _ + image2_iUnion₂_right .. @[to_additive] theorem iInter_div_subset (s : ι → Set α) (t : Set α) : (⋂ i, s i) / t ⊆ ⋂ i, s i / t := - image2_iInter_subset_left _ _ _ + image2_iInter_subset_left .. @[to_additive] theorem div_iInter_subset (s : Set α) (t : ι → Set α) : (s / ⋂ i, t i) ⊆ ⋂ i, s / t i := - image2_iInter_subset_right _ _ _ + image2_iInter_subset_right .. + +@[to_additive] +theorem sInter_div_subset (S : Set (Set α)) (t : Set α) : ⋂₀ S / t ⊆ ⋂ s ∈ S, s / t := + image2_sInter_subset_left .. + +@[to_additive] +theorem div_sInter_subset (s : Set α) (T : Set (Set α)) : s / ⋂₀ T ⊆ ⋂ t ∈ T, s / t := + image2_sInter_subset_right .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem iInter₂_div_subset (s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) / t ⊆ ⋂ (i) (j), s i j / t := - image2_iInter₂_subset_left _ _ _ + image2_iInter₂_subset_left .. /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ @[to_additive] theorem div_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set α) : (s / ⋂ (i) (j), t i j) ⊆ ⋂ (i) (j), s / t i j := - image2_iInter₂_subset_right _ _ _ + image2_iInter₂_subset_right .. end Div @@ -691,35 +731,51 @@ lemma iUnion_smul_right_image : ⋃ a ∈ t, (· • a) '' s = s • t := iUnion @[to_additive] lemma iUnion_smul (s : ι → Set α) (t : Set β) : (⋃ i, s i) • t = ⋃ i, s i • t := - image2_iUnion_left _ _ _ + image2_iUnion_left .. @[to_additive] lemma smul_iUnion (s : Set α) (t : ι → Set β) : (s • ⋃ i, t i) = ⋃ i, s • t i := - image2_iUnion_right _ _ _ + image2_iUnion_right .. + +@[to_additive] +lemma sUnion_smul (S : Set (Set α)) (t : Set β) : ⋃₀ S • t = ⋃ s ∈ S, s • t := + image2_sUnion_left .. + +@[to_additive] +lemma smul_sUnion (s : Set α) (T : Set (Set β)) : s • ⋃₀ T = ⋃ t ∈ T, s • t := + image2_sUnion_right .. @[to_additive] lemma iUnion₂_smul (s : ∀ i, κ i → Set α) (t : Set β) : - (⋃ i, ⋃ j, s i j) • t = ⋃ i, ⋃ j, s i j • t := image2_iUnion₂_left _ _ _ + (⋃ i, ⋃ j, s i j) • t = ⋃ i, ⋃ j, s i j • t := image2_iUnion₂_left .. @[to_additive] lemma smul_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set β) : - (s • ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s • t i j := image2_iUnion₂_right _ _ _ + (s • ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s • t i j := image2_iUnion₂_right .. @[to_additive] lemma iInter_smul_subset (s : ι → Set α) (t : Set β) : (⋂ i, s i) • t ⊆ ⋂ i, s i • t := - image2_iInter_subset_left _ _ _ + image2_iInter_subset_left .. @[to_additive] lemma smul_iInter_subset (s : Set α) (t : ι → Set β) : (s • ⋂ i, t i) ⊆ ⋂ i, s • t i := - image2_iInter_subset_right _ _ _ + image2_iInter_subset_right .. + +@[to_additive] +lemma sInter_smul_subset (S : Set (Set α)) (t : Set β) : ⋂₀ S • t ⊆ ⋂ s ∈ S, s • t := + image2_sInter_left_subset S t (fun a x => a • x) + +@[to_additive] +lemma smul_sInter_subset (s : Set α) (T : Set (Set β)) : s • ⋂₀ T ⊆ ⋂ t ∈ T, s • t := + image2_sInter_right_subset s T (fun a x => a • x) @[to_additive] lemma iInter₂_smul_subset (s : ∀ i, κ i → Set α) (t : Set β) : - (⋂ i, ⋂ j, s i j) • t ⊆ ⋂ i, ⋂ j, s i j • t := image2_iInter₂_subset_left _ _ _ + (⋂ i, ⋂ j, s i j) • t ⊆ ⋂ i, ⋂ j, s i j • t := image2_iInter₂_subset_left .. @[to_additive] lemma smul_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set β) : - (s • ⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, s • t i j := image2_iInter₂_subset_right _ _ _ + (s • ⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, s • t i j := image2_iInter₂_subset_right .. @[to_additive] lemma smul_set_subset_smul {s : Set α} : a ∈ s → a • t ⊆ s • t := image_subset_image2_right @@ -757,7 +813,7 @@ lemma smul_set_subset_iff : a • s ⊆ t ↔ ∀ ⦃b⦄, b ∈ s → a • b @[to_additive] lemma smul_set_union : a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂ := - image_union _ _ _ + image_union .. @[to_additive] lemma smul_set_insert (a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s) := @@ -765,7 +821,7 @@ lemma smul_set_insert (a : α) (b : β) (s : Set β) : a • insert b s = insert @[to_additive] lemma smul_set_inter_subset : a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂ := - image_inter_subset _ _ _ + image_inter_subset .. @[to_additive] lemma smul_set_iUnion (a : α) (s : ι → Set β) : a • ⋃ i, s i = ⋃ i, a • s i := @@ -773,15 +829,23 @@ lemma smul_set_iUnion (a : α) (s : ι → Set β) : a • ⋃ i, s i = ⋃ i, a @[to_additive] lemma smul_set_iUnion₂ (a : α) (s : ∀ i, κ i → Set β) : - a • ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a • s i j := image_iUnion₂ _ _ + a • ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a • s i j := image_iUnion₂ .. + +@[to_additive] +lemma smul_set_sUnion (a : α) (S : Set (Set β)) : a • ⋃₀ S = ⋃ s ∈ S, a • s := by + rw [sUnion_eq_biUnion, smul_set_iUnion₂] @[to_additive] lemma smul_set_iInter_subset (a : α) (t : ι → Set β) : a • ⋂ i, t i ⊆ ⋂ i, a • t i := - image_iInter_subset _ _ + image_iInter_subset .. + +@[to_additive] +lemma smul_set_sInter_subset (a : α) (S : Set (Set β)) : + a • ⋂₀ S ⊆ ⋂ s ∈ S, a • s := image_sInter_subset .. @[to_additive] lemma smul_set_iInter₂_subset (a : α) (t : ∀ i, κ i → Set β) : - a • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a • t i j := image_iInter₂_subset _ _ + a • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a • t i j := image_iInter₂_subset .. @[to_additive] lemma Nonempty.smul_set : s.Nonempty → (a • s).Nonempty := Nonempty.image _ @@ -797,7 +861,7 @@ lemma range_smul_range {ι κ : Type*} [SMul α β] (b : ι → α) (c : κ → @[to_additive] lemma smul_set_range [SMul α β] {ι : Sort*} (a : α) (f : ι → β) : a • range f = range fun i ↦ a • f i := - (range_comp _ _).symm + (range_comp ..).symm @[to_additive] lemma range_smul [SMul α β] {ι : Sort*} (a : α) (f : ι → β) : range (fun i ↦ a • f i) = a • range f := (smul_set_range ..).symm @@ -863,28 +927,40 @@ lemma iUnion_vsub_left_image : ⋃ a ∈ s, (a -ᵥ ·) '' t = s -ᵥ t := iUnio lemma iUnion_vsub_right_image : ⋃ a ∈ t, (· -ᵥ a) '' s = s -ᵥ t := iUnion_image_right _ lemma iUnion_vsub (s : ι → Set β) (t : Set β) : (⋃ i, s i) -ᵥ t = ⋃ i, s i -ᵥ t := - image2_iUnion_left _ _ _ + image2_iUnion_left .. lemma vsub_iUnion (s : Set β) (t : ι → Set β) : (s -ᵥ ⋃ i, t i) = ⋃ i, s -ᵥ t i := - image2_iUnion_right _ _ _ + image2_iUnion_right .. + +lemma sUnion_vsub (S : Set (Set β)) (t : Set β) : ⋃₀ S -ᵥ t = ⋃ s ∈ S, s -ᵥ t := + image2_sUnion_left .. + +lemma vsub_sUnion (s : Set β) (T : Set (Set β)) : s -ᵥ ⋃₀ T = ⋃ t ∈ T, s -ᵥ t := + image2_sUnion_right .. lemma iUnion₂_vsub (s : ∀ i, κ i → Set β) (t : Set β) : - (⋃ i, ⋃ j, s i j) -ᵥ t = ⋃ i, ⋃ j, s i j -ᵥ t := image2_iUnion₂_left _ _ _ + (⋃ i, ⋃ j, s i j) -ᵥ t = ⋃ i, ⋃ j, s i j -ᵥ t := image2_iUnion₂_left .. lemma vsub_iUnion₂ (s : Set β) (t : ∀ i, κ i → Set β) : - (s -ᵥ ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s -ᵥ t i j := image2_iUnion₂_right _ _ _ + (s -ᵥ ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s -ᵥ t i j := image2_iUnion₂_right .. lemma iInter_vsub_subset (s : ι → Set β) (t : Set β) : (⋂ i, s i) -ᵥ t ⊆ ⋂ i, s i -ᵥ t := - image2_iInter_subset_left _ _ _ + image2_iInter_subset_left .. lemma vsub_iInter_subset (s : Set β) (t : ι → Set β) : (s -ᵥ ⋂ i, t i) ⊆ ⋂ i, s -ᵥ t i := - image2_iInter_subset_right _ _ _ + image2_iInter_subset_right .. + +lemma sInter_vsub_subset (S : Set (Set β)) (t : Set β) : ⋂₀ S -ᵥ t ⊆ ⋂ s ∈ S, s -ᵥ t := + image2_sInter_subset_left .. + +lemma vsub_sInter_subset (s : Set β) (T : Set (Set β)) : s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t := + image2_sInter_subset_right .. lemma iInter₂_vsub_subset (s : ∀ i, κ i → Set β) (t : Set β) : - (⋂ i, ⋂ j, s i j) -ᵥ t ⊆ ⋂ i, ⋂ j, s i j -ᵥ t := image2_iInter₂_subset_left _ _ _ + (⋂ i, ⋂ j, s i j) -ᵥ t ⊆ ⋂ i, ⋂ j, s i j -ᵥ t := image2_iInter₂_subset_left .. lemma vsub_iInter₂_subset (s : Set β) (t : ∀ i, κ i → Set β) : - s -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j := image2_iInter₂_subset_right _ _ _ + s -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j := image2_iInter₂_subset_right .. end VSub @@ -1195,12 +1271,12 @@ theorem preimage_mul_right_one' : (· * b⁻¹) ⁻¹' 1 = {b} := by simp @[to_additive (attr := simp)] theorem mul_univ (hs : s.Nonempty) : s * (univ : Set α) = univ := let ⟨a, ha⟩ := hs - eq_univ_of_forall fun b => ⟨a, ha, a⁻¹ * b, trivial, mul_inv_cancel_left _ _⟩ + eq_univ_of_forall fun b => ⟨a, ha, a⁻¹ * b, trivial, mul_inv_cancel_left ..⟩ @[to_additive (attr := simp)] theorem univ_mul (ht : t.Nonempty) : (univ : Set α) * t = univ := let ⟨a, ha⟩ := ht - eq_univ_of_forall fun b => ⟨b * a⁻¹, trivial, a, ha, inv_mul_cancel_right _ _⟩ + eq_univ_of_forall fun b => ⟨b * a⁻¹, trivial, a, ha, inv_mul_cancel_right ..⟩ end Group @@ -1217,12 +1293,12 @@ lemma mul_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) rintro _ ⟨a, ha, b, hb, rfl⟩ obtain ⟨a, rfl⟩ := hs ha obtain ⟨b, rfl⟩ := ht hb - exact ⟨a * b, map_mul _ _ _⟩ + exact ⟨a * b, map_mul ..⟩ @[to_additive] theorem preimage_mul_preimage_subset {s t : Set β} : m ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t) := by rintro _ ⟨_, _, _, _, rfl⟩ - exact ⟨_, ‹_›, _, ‹_›, (map_mul m _ _).symm⟩ + exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩ @[to_additive] lemma preimage_mul (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : @@ -1246,12 +1322,12 @@ lemma div_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) rintro _ ⟨a, ha, b, hb, rfl⟩ obtain ⟨a, rfl⟩ := hs ha obtain ⟨b, rfl⟩ := ht hb - exact ⟨a / b, map_div _ _ _⟩ + exact ⟨a / b, map_div ..⟩ @[to_additive] theorem preimage_div_preimage_subset {s t : Set β} : m ⁻¹' s / m ⁻¹' t ⊆ m ⁻¹' (s / t) := by rintro _ ⟨_, _, _, _, rfl⟩ - exact ⟨_, ‹_›, _, ‹_›, (map_div m _ _).symm⟩ + exact ⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩ @[to_additive] lemma preimage_div (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean index fbff041791382..b6f29fa406fdf 100644 --- a/Mathlib/Data/Set/Lattice.lean +++ b/Mathlib/Data/Set/Lattice.lean @@ -1243,6 +1243,14 @@ theorem image_sInter_subset (S : Set (Set α)) (f : α → β) : f '' ⋂₀ S rw [sInter_eq_biInter] apply image_iInter₂_subset +theorem image2_sInter_right_subset (t : Set α) (S : Set (Set β)) (f : α → β → γ) : + image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, image2 f t s := by + aesop + +theorem image2_sInter_left_subset (S : Set (Set α)) (t : Set β) (f : α → β → γ) : + image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t := by + aesop + /-! ### `restrictPreimage` -/ @@ -1575,6 +1583,14 @@ theorem image2_iUnion_right (s : Set α) (t : ι → Set β) : image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i) := by simp only [← image_prod, prod_iUnion, image_iUnion] +theorem image2_sUnion_left (S : Set (Set α)) (t : Set β) : + image2 f (⋃₀ S) t = ⋃ s ∈ S, image2 f s t := by + aesop + +theorem image2_sUnion_right (s : Set α) (T : Set (Set β)) : + image2 f s (⋃₀ T) = ⋃ t ∈ T, image2 f s t := by + aesop + /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ theorem image2_iUnion₂_left (s : ∀ i, κ i → Set α) (t : Set β) : @@ -1610,6 +1626,16 @@ theorem image2_iInter₂_subset_right (s : Set α) (t : ∀ i, κ i → Set β) simp_rw [image2_subset_iff, mem_iInter] exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _) +theorem image2_sInter_subset_left (S : Set (Set α)) (t : Set β) : + image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t := by + rw [sInter_eq_biInter] + exact image2_iInter₂_subset_left .. + +theorem image2_sInter_subset_right (s : Set α) (T : Set (Set β)) : + image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t := by + rw [sInter_eq_biInter] + exact image2_iInter₂_subset_right .. + theorem prod_eq_biUnion_left : s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t := by rw [iUnion_image_left, image2_mk_eq_prod]