# N-ary images of finsets #

This file defines `Finset.image₂`, the binary image of finsets. This is the finset version of `Set.image2`. This is mostly useful to define pointwise operations.

## Notes #

This file is very similar to `Data.Set.NAry`, `Order.Filter.NAry` and `Data.Option.NAry`. Please keep them in sync.

We do not define `Finset.image₃` as its only purpose would be to prove properties of `Finset.image₂` and `Set.image2` already fulfills this task.

source
def Finset.image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β) :
Finset γ

The image of a binary function `f : α → β → γ` as a function `Finset α → Finset β → Finset γ`. Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.

Equations

- Finset.image₂ f s t = Finset.image (Function.uncurry f) (s ×ˢ t)

Instances For

source
@[simp]
theorem Finset.mem_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {c : γ} :
c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c
source
@[simp]
theorem Finset.coe_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β) :
↑(image₂ f s t) = Set.image2 f ↑s ↑t
source
theorem Finset.card_image₂_le {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β) :
(image₂ f s t).card ≤ s.card * t.card
source
theorem Finset.card_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} :
(image₂ f s t).card = s.card * t.card ↔ Set.InjOn (fun (x : α × β) => f x.1 x.2) (↑s ×ˢ ↑t)
source
theorem Finset.card_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} (hf : Function.Injective2 f) (s : Finset α) (t : Finset β) :
(image₂ f s t).card = s.card * t.card
source
theorem Finset.mem_image₂_of_mem {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {a : α} {b : β} (ha : a ∈ s) (hb : b ∈ t) :
f a b ∈ image₂ f s t
source
theorem Finset.mem_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {a : α} {b : β} (hf : Function.Injective2 f) :
f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
source
theorem Finset.image₂_subset {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t t' : Finset β} (hs : s ⊆ s') (ht : t ⊆ t') :
image₂ f s t ⊆ image₂ f s' t'
source
theorem Finset.image₂_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β} (ht : t ⊆ t') :
image₂ f s t ⊆ image₂ f s t'
source
theorem Finset.image₂_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β} (hs : s ⊆ s') :
image₂ f s t ⊆ image₂ f s' t
source
theorem Finset.image_subset_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {b : β} (hb : b ∈ t) :
image (fun (a : α) => f a b) s ⊆ image₂ f s t
source
theorem Finset.image_subset_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {a : α} (ha : a ∈ s) :
image (fun (b : β) => f a b) t ⊆ image₂ f s t
source
theorem Finset.forall_mem_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {p : γ → Prop} :
(∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
source
theorem Finset.exists_mem_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {p : γ → Prop} :
(∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)
source
@[simp]
theorem Finset.image₂_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {u : Finset γ} :
image₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
source
theorem Finset.image₂_subset_iff_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {u : Finset γ} :
image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun (b : β) => f a b) t ⊆ u
source
theorem Finset.image₂_subset_iff_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {u : Finset γ} :
image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun (a : α) => f a b) s ⊆ u
source
@[simp]
theorem Finset.image₂_nonempty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} :
(image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
theorem Finset.Nonempty.image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} (hs : s.Nonempty) (ht : t.Nonempty) :
(Finset.image₂ f s t).Nonempty
source
theorem Finset.Nonempty.of_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} (h : (Finset.image₂ f s t).Nonempty) :
s.Nonempty
source
theorem Finset.Nonempty.of_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} (h : (Finset.image₂ f s t).Nonempty) :
t.Nonempty
source
@[simp]
theorem Finset.image₂_empty_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {t : Finset β} :
image₂ f ∅ t = ∅
source
@[simp]
theorem Finset.image₂_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} :
image₂ f s ∅ = ∅
source
@[simp]
theorem Finset.image₂_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} :
image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Finset.image₂_singleton_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {t : Finset β} {a : α} :
image₂ f {a} t = image (fun (b : β) => f a b) t
source
@[simp]
theorem Finset.image₂_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {b : β} :
image₂ f s {b} = image (fun (a : α) => f a b) s
source
theorem Finset.image₂_singleton_left' {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {t : Finset β} {a : α} :
image₂ f {a} t = image (f a) t
source
theorem Finset.image₂_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {a : α} {b : β} :
image₂ f {a} {b} = {f a b}
source
theorem Finset.image₂_union_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β} [DecidableEq α] :
image₂ f (s ∪ s') t = image₂ f s t ∪ image₂ f s' t
source
theorem Finset.image₂_union_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β} [DecidableEq β] :
image₂ f s (t ∪ t') = image₂ f s t ∪ image₂ f s t'
source
@[simp]
theorem Finset.image₂_insert_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {a : α} [DecidableEq α] :
image₂ f (insert a s) t = image (fun (b : β) => f a b) t ∪ image₂ f s t
source
@[simp]
theorem Finset.image₂_insert_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {b : β} [DecidableEq β] :
image₂ f s (insert b t) = image (fun (a : α) => f a b) s ∪ image₂ f s t
source
theorem Finset.image₂_inter_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β} [DecidableEq α] (hf : Function.Injective2 f) :
image₂ f (s ∩ s') t = image₂ f s t ∩ image₂ f s' t
source
theorem Finset.image₂_inter_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β} [DecidableEq β] (hf : Function.Injective2 f) :
image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t'
source
theorem Finset.image₂_inter_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β} [DecidableEq α] :
image₂ f (s ∩ s') t ⊆ image₂ f s t ∩ image₂ f s' t
source
theorem Finset.image₂_inter_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β} [DecidableEq β] :
image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t'
source
theorem Finset.image₂_congr {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f f' : α → β → γ} {s : Finset α} {t : Finset β} (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) :
image₂ f s t = image₂ f' s t
source
theorem Finset.image₂_congr' {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f f' : α → β → γ} {s : Finset α} {t : Finset β} (h : ∀ (a : α) (b : β), f a b = f' a b) :
image₂ f s t = image₂ f' s t

A common special case of `image₂_congr`

source
theorem Finset.card_image₂_singleton_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} (t : Finset β) {a : α} (hf : Function.Injective (f a)) :
(image₂ f {a} t).card = t.card
source
theorem Finset.card_image₂_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} (s : Finset α) {b : β} (hf : Function.Injective fun (a : α) => f a b) :
(image₂ f s {b}).card = s.card
source
theorem Finset.image₂_singleton_inter {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {a : α} [DecidableEq β] (t₁ t₂ : Finset β) (hf : Function.Injective (f a)) :
image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂
source
theorem Finset.image₂_inter_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {b : β} [DecidableEq α] (s₁ s₂ : Finset α) (hf : Function.Injective fun (a : α) => f a b) :
image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}
source
theorem Finset.card_le_card_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} (t : Finset β) {a : α} {s : Finset α} (ha : a ∈ s) (hf : Function.Injective (f a)) :
t.card ≤ (image₂ f s t).card
source
theorem Finset.card_le_card_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} (s : Finset α) {b : β} {t : Finset β} (hb : b ∈ t) (hf : Function.Injective fun (x : α) => f x b) :
s.card ≤ (image₂ f s t).card
source
theorem Finset.biUnion_image_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} :
(s.biUnion fun (a : α) => image (f a) t) = image₂ f s t
source
theorem Finset.biUnion_image_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} :
(t.biUnion fun (b : β) => image (fun (a : α) => f a b) s) = image₂ f s t

### Algebraic replacement rules #

A collection of lemmas to transfer associativity, commutativity, distributivity, ... of operations to the associativity, commutativity, distributivity, ... of `Finset.image₂` of those operations.

The proof pattern is `image₂_lemma operation_lemma`. For example, `image₂_comm mul_comm` proves that `image₂ (*) f g = image₂ (*) g f` in a `CommSemigroup`.

source
theorem Finset.image_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] (f : α → β → γ) (g : γ → δ) :
image g (image₂ f s t) = image₂ (fun (a : α) (b : β) => g (f a b)) s t
source
theorem Finset.image₂_image_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] (f : γ → β → δ) (g : α → γ) :
image₂ f (image g s) t = image₂ (fun (a : α) (b : β) => f (g a) b) s t
source
theorem Finset.image₂_image_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] (f : α → γ → δ) (g : β → γ) :
image₂ f s (image g t) = image₂ (fun (a : α) (b : β) => f a (g b)) s t
source
@[simp]
theorem Finset.image₂_mk_eq_product {α : Type u_1} {β : Type u_3} [DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset β) :
image₂ Prod.mk s t = s ×ˢ t
source
@[simp]
theorem Finset.image₂_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α × β → γ) (s : Finset α) (t : Finset β) :
image₂ (Function.curry f) s t = image f (s ×ˢ t)
source
@[simp]
theorem Finset.image_uncurry_product {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β) :
image (Function.uncurry f) (s ×ˢ t) = image₂ f s t
source
theorem Finset.image₂_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β) :
image₂ f s t = image₂ (fun (a : β) (b : α) => f b a) t s
source
@[simp]
theorem Finset.image₂_left {α : Type u_1} {β : Type u_3} {s : Finset α} {t : Finset β} [DecidableEq α] (h : t.Nonempty) :
image₂ (fun (x : α) (x_1 : β) => x) s t = s
source
@[simp]
theorem Finset.image₂_right {α : Type u_1} {β : Type u_3} {s : Finset α} {t : Finset β} [DecidableEq β] (h : s.Nonempty) :
image₂ (fun (x : α) (y : β) => y) s t = t
source
theorem Finset.image₂_assoc {α : Type u_1} {β : Type u_3} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} [DecidableEq ε] [DecidableEq ε'] {s : Finset α} {t : Finset β} [DecidableEq δ] {γ : Type u_14} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'} (h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) :
image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u)
source
theorem Finset.image₂_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} {g : β → α → γ} (h_comm : ∀ (a : α) (b : β), f a b = g b a) :
image₂ f s t = image₂ g t s
source
theorem Finset.image₂_left_comm {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [DecidableEq δ'] [DecidableEq ε] {s : Finset α} {t : Finset β} [DecidableEq δ] {γ : Type u_14} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε} (h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) :
image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u)
source
theorem Finset.image₂_right_comm {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [DecidableEq δ'] [DecidableEq ε] {s : Finset α} {t : Finset β} [DecidableEq δ] {γ : Type u_14} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε} (h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) :
image₂ f (image₂ g s t) u = image₂ g' (image₂ f' s u) t
source
theorem Finset.image₂_image₂_image₂_comm {α : Type u_1} {β : Type u_3} {ε : Type u_9} {ε' : Type u_10} {ζ : Type u_11} {ζ' : Type u_12} {ν : Type u_13} [DecidableEq ε] [DecidableEq ε'] {s : Finset α} {t : Finset β} {γ : Type u_14} {δ : Type u_15} {u : Finset γ} {v : Finset δ} [DecidableEq ζ] [DecidableEq ζ'] [DecidableEq ν] {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ} {f' : ε' → ζ' → ν} {g' : α → γ → ε'} {h' : β → δ → ζ'} (h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)) :
image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v)
source
theorem Finset.image_image₂_distrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [DecidableEq α'] [DecidableEq β'] [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) :
image g (image₂ f s t) = image₂ f' (image g₁ s) (image g₂ t)
source
theorem Finset.image_image₂_distrib_left {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq α'] [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b) :
image g (image₂ f s t) = image₂ f' (image g' s) t

Symmetric statement to `Finset.image₂_image_left_comm`.

source
theorem Finset.image_image₂_distrib_right {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [DecidableEq β'] [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γ → δ} {f' : α → β' → δ} {g' : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)) :
image g (image₂ f s t) = image₂ f' s (image g' t)

Symmetric statement to `Finset.image_image₂_right_comm`.

source
theorem Finset.image₂_image_left_comm {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq α'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ} (h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)) :
image₂ f (image g s) t = image g' (image₂ f' s t)

Symmetric statement to `Finset.image_image₂_distrib_left`.

source
theorem Finset.image_image₂_right_comm {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [DecidableEq β'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ} (h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)) :
image₂ f s (image g t) = image g' (image₂ f' s t)

Symmetric statement to `Finset.image_image₂_distrib_right`.

source
theorem Finset.image₂_distrib_subset_left {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9} [DecidableEq β'] [DecidableEq γ'] [DecidableEq ε] {s : Finset α} {t : Finset β} [DecidableEq δ] {γ : Type u_14} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε} (h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) :
image₂ f s (image₂ g t u) ⊆ image₂ g' (image₂ f₁ s t) (image₂ f₂ s u)

The other direction does not hold because of the `s`-`s` cross terms on the RHS.

source
theorem Finset.image₂_distrib_subset_right {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {δ : Type u_7} {ε : Type u_9} [DecidableEq α'] [DecidableEq β'] [DecidableEq ε] {s : Finset α} {t : Finset β} [DecidableEq δ] {γ : Type u_14} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε} (h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) :
image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u)

The other direction does not hold because of the `u`-`u` cross terms on the RHS.

source
theorem Finset.image_image₂_antidistrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [DecidableEq α'] [DecidableEq β'] [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) :
image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)
source
theorem Finset.image_image₂_antidistrib_left {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [DecidableEq β'] [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γ → δ} {f' : β' → α → δ} {g' : β → β'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a) :
image g (image₂ f s t) = image₂ f' (image g' t) s

Symmetric statement to `Finset.image₂_image_left_anticomm`.

source
theorem Finset.image_image₂_antidistrib_right {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq α'] [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γ → δ} {f' : β → α' → δ} {g' : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)) :
image g (image₂ f s t) = image₂ f' t (image g' s)

Symmetric statement to `Finset.image_image₂_right_anticomm`.

source
theorem Finset.image₂_image_left_anticomm {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq α'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ} (h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)) :
image₂ f (image g s) t = image g' (image₂ f' t s)

Symmetric statement to `Finset.image_image₂_antidistrib_left`.

source
theorem Finset.image_image₂_right_anticomm {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [DecidableEq β'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ} (h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)) :
image₂ f s (image g t) = image g' (image₂ f' t s)

Symmetric statement to `Finset.image_image₂_antidistrib_right`.

source
theorem Finset.image₂_left_identity {α : Type u_1} {γ : Type u_5} [DecidableEq γ] {f : α → γ → γ} {a : α} (h : ∀ (b : γ), f a b = b) (t : Finset γ) :
image₂ f {a} t = t

If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for `Finset.image₂ f`.

source
theorem Finset.image₂_right_identity {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : γ → β → γ} {b : β} (h : ∀ (a : γ), f a b = a) (s : Finset γ) :
image₂ f s {b} = s

If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for `Finset.image₂ f`.

source
theorem Finset.card_dvd_card_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} (hf : ∀ a ∈ s, Function.Injective (f a)) (hs : ((fun (a : α) => image (f a) t) '' ↑s).PairwiseDisjoint id) :
t.card ∣ (image₂ f s t).card

If each partial application of `f` is injective, and images of `s` under those partial applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of `Finset.image₂ f s t`.

source
theorem Finset.card_dvd_card_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} (hf : ∀ b ∈ t, Function.Injective fun (a : α) => f a b) (ht : ((fun (b : β) => image (fun (a : α) => f a b) s) '' ↑t).PairwiseDisjoint id) :
s.card ∣ (image₂ f s t).card

If each partial application of `f` is injective, and images of `t` under those partial applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of `Finset.image₂ f s t`.

source
theorem Finset.subset_set_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {u : Finset γ} {s : Set α} {t : Set β} (hu : ↑u ⊆ Set.image2 f s t) :
∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

If a `Finset` is a subset of the image of two `Set`s under a binary operation, then it is a subset of the `Finset.image₂` of two `Finset` subsets of these `Set`s.

source
theorem Finset.image₂_inter_union_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t t' : Finset β} [DecidableEq α] [DecidableEq β] :
image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t'
source
theorem Finset.image₂_union_inter_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t t' : Finset β} [DecidableEq α] [DecidableEq β] :
image₂ f (s ∪ s') (t ∩ t') ⊆ image₂ f s t ∪ image₂ f s' t'
source
theorem Finset.image₂_inter_union_subset {α : Type u_1} {β : Type u_3} [DecidableEq α] [DecidableEq β] {f : α → α → β} {s t : Finset α} (hf : ∀ (a b : α), f a b = f b a) :
image₂ f (s ∩ t) (s ∪ t) ⊆ image₂ f s t
source
theorem Finset.image₂_union_inter_subset {α : Type u_1} {β : Type u_3} [DecidableEq α] [DecidableEq β] {f : α → α → β} {s t : Finset α} (hf : ∀ (a b : α), f a b = f b a) :
image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t
source
@[simp]
theorem Finset.sup'_image₂_le {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeSup δ] {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
(image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
source
theorem Finset.sup'_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeSup δ] (g : γ → δ) (h : (image₂ f s t).Nonempty) :
(image₂ f s t).sup' h g = s.sup' ⋯ fun (x : α) => t.sup' ⋯ fun (x_1 : β) => g (f x x_1)
source
theorem Finset.sup'_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeSup δ] (g : γ → δ) (h : (image₂ f s t).Nonempty) :
(image₂ f s t).sup' h g = t.sup' ⋯ fun (y : β) => s.sup' ⋯ fun (x : α) => g (f x y)
source
@[simp]
theorem Finset.sup_image₂_le {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeSup δ] [OrderBot δ] {g : γ → δ} {a : δ} :
(image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
source
theorem Finset.sup_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} (s : Finset α) (t : Finset β) [SemilatticeSup δ] [OrderBot δ] (g : γ → δ) :
(image₂ f s t).sup g = s.sup fun (x : α) => t.sup fun (x_1 : β) => g (f x x_1)
source
theorem Finset.sup_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} (s : Finset α) (t : Finset β) [SemilatticeSup δ] [OrderBot δ] (g : γ → δ) :
(image₂ f s t).sup g = t.sup fun (y : β) => s.sup fun (x : α) => g (f x y)
source
@[simp]
theorem Finset.le_inf'_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeInf δ] {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
source
theorem Finset.inf'_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeInf δ] (g : γ → δ) (h : (image₂ f s t).Nonempty) :
(image₂ f s t).inf' h g = s.inf' ⋯ fun (x : α) => t.inf' ⋯ fun (x_1 : β) => g (f x x_1)
source
theorem Finset.inf'_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeInf δ] (g : γ → δ) (h : (image₂ f s t).Nonempty) :
(image₂ f s t).inf' h g = t.inf' ⋯ fun (y : β) => s.inf' ⋯ fun (x : α) => g (f x y)
source
@[simp]
theorem Finset.le_inf_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [SemilatticeInf δ] [OrderTop δ] {g : γ → δ} {a : δ} :
a ≤ (image₂ f s t).inf g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
source
theorem Finset.inf_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} (s : Finset α) (t : Finset β) [SemilatticeInf δ] [OrderTop δ] (g : γ → δ) :
(image₂ f s t).inf g = s.inf fun (x : α) => t.inf (g ∘ f x)
source
theorem Finset.inf_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {f : α → β → γ} (s : Finset α) (t : Finset β) [SemilatticeInf δ] [OrderTop δ] (g : γ → δ) :
(image₂ f s t).inf g = t.inf fun (y : β) => s.inf fun (x : α) => g (f x y)
source
theorem Fintype.piFinset_image₂ {ι : Type u_14} {α : ι → Type u_15} {β : ι → Type u_16} {γ : ι → Type u_17} [DecidableEq ι] [Fintype ι] [(i : ι) → DecidableEq (γ i)] (f : (i : ι) → α i → β i → γ i) (s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)) :
(piFinset fun (i : ι) => Finset.image₂ (f i) (s i) (t i)) = Finset.image₂ (fun (a : (a : ι) → α a) (b : (a : ι) → β a) (i : ι) => f i (a i) (b i)) (piFinset s) (piFinset t)
source
@[simp]
theorem Set.toFinset_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β) [Fintype ↑s] [Fintype ↑t] [Fintype ↑(image2 f s t)] :
(image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset
source
theorem Set.Finite.toFinset_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {s : Set α} {t : Set β} (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) (hf : (image2 f s t).Finite := ⋯) :
hf.toFinset = Finset.image₂ f hs.toFinset ht.toFinset