# mathlib3documentation

data.finset.n_ary

# N-ary images of finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.n_ary, order.filter.n_ary and data.option.n_ary. 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.

def finset.image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α β γ) (s : finset α) (t : 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
@[simp]
theorem finset.mem_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {c : γ} :
c t (a : α) (b : β), a s b t f a b = c
@[simp, norm_cast]
theorem finset.coe_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α β γ) (s : finset α) (t : finset β) :
s t) = s t
theorem finset.card_image₂_le {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α β γ) (s : finset α) (t : finset β) :
s t).card s.card * t.card
theorem finset.card_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} :
s t).card = s.card * t.card set.inj_on (λ (x : α × β), f x.fst x.snd) (s ×ˢ t)
theorem finset.card_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} (hf : function.injective2 f) (s : finset α) (t : finset β) :
s t).card = s.card * t.card
theorem finset.mem_image₂_of_mem {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {a : α} {b : β} (ha : a s) (hb : b t) :
f a b t
theorem finset.mem_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {a : α} {b : β} (hf : function.injective2 f) :
f a b t a s b t
theorem finset.image₂_subset {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t t' : finset β} (hs : s s') (ht : t t') :
t s' t'
theorem finset.image₂_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t t' : finset β} (ht : t t') :
t t'
theorem finset.image₂_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t : finset β} (hs : s s') :
t s' t
theorem finset.image_subset_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {b : β} (hb : b t) :
finset.image (λ (a : α), f a b) s t
theorem finset.image_subset_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {a : α} (ha : a s) :
finset.image (λ (b : β), f a b) t t
theorem finset.forall_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {p : γ Prop} :
( (z : γ), z t p z) (x : α), x s (y : β), y t p (f x y)
@[simp]
theorem finset.image₂_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {u : finset γ} :
t u (x : α), x s (y : β), y t f x y u
theorem finset.image₂_subset_iff_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {u : finset γ} :
t u (a : α), a s finset.image (λ (b : β), f a b) t u
theorem finset.image₂_subset_iff_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {u : finset γ} :
t u (b : β), b t finset.image (λ (a : α), f a b) s u
@[simp]
theorem finset.image₂_nonempty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} :
s t).nonempty
theorem finset.nonempty.image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} (hs : s.nonempty) (ht : t.nonempty) :
s t).nonempty
theorem finset.nonempty.of_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} (h : s t).nonempty) :
theorem finset.nonempty.of_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} (h : s t).nonempty) :
@[simp]
theorem finset.image₂_empty_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {t : finset β} :
t =
@[simp]
theorem finset.image₂_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} :
@[simp]
theorem finset.image₂_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} :
t = s = t =
@[simp]
theorem finset.image₂_singleton_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {t : finset β} {a : α} :
{a} t = finset.image (λ (b : β), f a b) t
@[simp]
theorem finset.image₂_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {b : β} :
{b} = finset.image (λ (a : α), f a b) s
theorem finset.image₂_singleton_left' {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {t : finset β} {a : α} :
{a} t = finset.image (f a) t
theorem finset.image₂_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {a : α} {b : β} :
{a} {b} = {f a b}
theorem finset.image₂_union_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t : finset β} [decidable_eq α] :
(s s') t = t s' t
theorem finset.image₂_union_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t t' : finset β} [decidable_eq β] :
(t t') = t t'
@[simp]
theorem finset.image₂_insert_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {a : α} [decidable_eq α] :
s) t = finset.image (λ (b : β), f a b) t t
@[simp]
theorem finset.image₂_insert_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {b : β} [decidable_eq β] :
t) = finset.image (λ (a : α), f a b) s t
theorem finset.image₂_inter_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t : finset β} [decidable_eq α] (hf : function.injective2 f) :
(s s') t = t s' t
theorem finset.image₂_inter_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t t' : finset β} [decidable_eq β] (hf : function.injective2 f) :
(t t') = t t'
theorem finset.image₂_inter_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t : finset β} [decidable_eq α] :
(s s') t t s' t
theorem finset.image₂_inter_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t t' : finset β} [decidable_eq β] :
(t t') t t'
theorem finset.image₂_congr {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f f' : α β γ} {s : finset α} {t : finset β} (h : (a : α), a s (b : β), b t f a b = f' a b) :
t = s t
theorem finset.image₂_congr' {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f f' : α β γ} {s : finset α} {t : finset β} (h : (a : α) (b : β), f a b = f' a b) :
t = s t

A common special case of image₂_congr

theorem finset.subset_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {u : finset γ} {s : set α} {t : set β} (hu : u s t) :
(s' : finset α) (t' : finset β), s' s t' t u s' t'
theorem finset.card_image₂_singleton_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} (t : finset β) {a : α} (hf : function.injective (f a)) :
{a} t).card = t.card
theorem finset.card_image₂_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} (s : finset α) {b : β} (hf : function.injective (λ (a : α), f a b)) :
s {b}).card = s.card
theorem finset.image₂_singleton_inter {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {a : α} [decidable_eq β] (t₁ t₂ : finset β) (hf : function.injective (f a)) :
{a} (t₁ t₂) = {a} t₁ {a} t₂
theorem finset.image₂_inter_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {b : β} [decidable_eq α] (s₁ s₂ : finset α) (hf : function.injective (λ (a : α), f a b)) :
(s₁ s₂) {b} = s₁ {b} s₂ {b}
theorem finset.card_le_card_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} (t : finset β) {s : finset α} (hs : s.nonempty) (hf : (a : α), function.injective (f a)) :
t.card s t).card
theorem finset.card_le_card_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} (s : finset α) {t : finset β} (ht : t.nonempty) (hf : (b : β), function.injective (λ (a : α), f a b)) :
s.card s t).card
theorem finset.bUnion_image_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} :
s.bUnion (λ (a : α), finset.image (f a) t) = t
theorem finset.bUnion_image_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} :
t.bUnion (λ (b : β), finset.image (λ (a : α), f a b) 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 comm_semigroup.

theorem finset.image_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [decidable_eq γ] [decidable_eq δ] {s : finset α} {t : finset β} (f : α β γ) (g : γ δ) :
s t) = finset.image₂ (λ (a : α) (b : β), g (f a b)) s t
theorem finset.image₂_image_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [decidable_eq γ] [decidable_eq δ] {s : finset α} {t : finset β} (f : γ β δ) (g : α γ) :
s) t = finset.image₂ (λ (a : α) (b : β), f (g a) b) s t
theorem finset.image₂_image_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [decidable_eq γ] [decidable_eq δ] {s : finset α} {t : finset β} (f : α γ δ) (g : β γ) :
t) = finset.image₂ (λ (a : α) (b : β), f a (g b)) s t
@[simp]
theorem finset.image₂_mk_eq_product {α : Type u_1} {β : Type u_3} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
= s ×ˢ t
@[simp]
theorem finset.image₂_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α × β γ) (s : finset α) (t : finset β) :
t = (s ×ˢ t)
@[simp]
theorem finset.image_uncurry_product {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α β γ) (s : finset α) (t : finset β) :
(s ×ˢ t) = t
theorem finset.image₂_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α β γ) (s : finset α) (t : finset β) :
t = finset.image₂ (λ (a : β) (b : α), f b a) t s
@[simp]
theorem finset.image₂_left {α : Type u_1} {β : Type u_3} {s : finset α} {t : finset β} [decidable_eq α] (h : t.nonempty) :
finset.image₂ (λ (x : α) (y : β), x) s t = s
@[simp]
theorem finset.image₂_right {α : Type u_1} {β : Type u_3} {s : finset α} {t : finset β} [decidable_eq β] (h : s.nonempty) :
finset.image₂ (λ (x : α) (y : β), y) s t = t
theorem finset.image₂_assoc {α : Type u_1} {β : Type u_3} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} [decidable_eq δ] [decidable_eq ε] [decidable_eq ε'] {s : finset α} {t : finset β} {γ : Type u_2} {u : finset γ} {f : δ γ ε} {g : α β δ} {f' : α ε' ε} {g' : β γ ε'} (h_assoc : (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) :
s t) u = s t u)
theorem finset.image₂_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} {g : β α γ} (h_comm : (a : α) (b : β), f a b = g b a) :
t = s
theorem finset.image₂_left_comm {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [decidable_eq δ] [decidable_eq δ'] [decidable_eq ε] {s : finset α} {t : finset β} {γ : Type u_2} {u : finset γ} {f : α δ ε} {g : β γ δ} {f' : α γ δ'} {g' : β δ' ε} (h_left_comm : (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) :
t u) = t s u)
theorem finset.image₂_right_comm {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [decidable_eq δ] [decidable_eq δ'] [decidable_eq ε] {s : finset α} {t : finset β} {γ : Type u_2} {u : finset γ} {f : δ γ ε} {g : α β δ} {f' : α γ δ'} {g' : δ' β ε} (h_right_comm : (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) :
s t) u = s u) t
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} [decidable_eq ε] [decidable_eq ε'] {s : finset α} {t : finset β} {γ : Type u_2} {δ : Type u_4} {u : finset γ} {v : finset δ} [decidable_eq ζ] [decidable_eq ζ'] [decidable_eq ν] {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)) :
s t) u v) = s u) t v)
theorem finset.image_image₂_distrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [decidable_eq α'] [decidable_eq β'] [decidable_eq γ] [decidable_eq δ] {f : α β γ} {s : finset α} {t : finset β} {g : γ δ} {f' : α' β' δ} {g₁ : α α'} {g₂ : β β'} (h_distrib : (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) :
s t) = (finset.image g₁ s) (finset.image g₂ t)
theorem finset.image_image₂_distrib_left {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [decidable_eq α'] [decidable_eq γ] [decidable_eq δ] {f : α β γ} {s : finset α} {t : finset β} {g : γ δ} {f' : α' β δ} {g' : α α'} (h_distrib : (a : α) (b : β), g (f a b) = f' (g' a) b) :
s t) = (finset.image g' s) t

Symmetric statement to finset.image₂_image_left_comm.

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

Symmetric statement to finset.image_image₂_right_comm.

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

Symmetric statement to finset.image_image₂_distrib_left.

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

Symmetric statement to finset.image_image₂_distrib_right.

theorem finset.image₂_distrib_subset_left {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9} [decidable_eq β'] [decidable_eq γ'] [decidable_eq δ] [decidable_eq ε] {s : finset α} {t : finset β} {γ : Type u_2} {u : finset γ} {f : α δ ε} {g : β γ δ} {f₁ : α β β'} {f₂ : α γ γ'} {g' : β' γ' ε} (h_distrib : (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) :
t u) s t) s u)

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

theorem finset.image₂_distrib_subset_right {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {δ : Type u_7} {ε : Type u_9} [decidable_eq α'] [decidable_eq β'] [decidable_eq δ] [decidable_eq ε] {s : finset α} {t : finset β} {γ : Type u_5} {u : finset γ} {f : δ γ ε} {g : α β δ} {f₁ : α γ α'} {f₂ : β γ β'} {g' : α' β' ε} (h_distrib : (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) :
s t) u s u) t u)

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

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

Symmetric statement to finset.image₂_image_left_anticomm.

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

Symmetric statement to finset.image_image₂_right_anticomm.

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

Symmetric statement to finset.image_image₂_antidistrib_left.

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

Symmetric statement to finset.image_image₂_antidistrib_right.

theorem finset.image₂_left_identity {α : Type u_1} {γ : Type u_5} [decidable_eq γ] {f : α γ γ} {a : α} (h : (b : γ), f a b = b) (t : finset γ) :
{a} t = t

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

theorem finset.image₂_right_identity {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : γ β γ} {b : β} (h : (a : γ), f a b = a) (s : finset γ) :
{b} = s

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

theorem finset.card_dvd_card_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} (hf : (a : α), a s function.injective (f a)) (hs : ((λ (a : α), finset.image (f a) t) '' s).pairwise_disjoint id) :
t.card 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.

theorem finset.card_dvd_card_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s : finset α} {t : finset β} (hf : (b : β), b t function.injective (λ (a : α), f a b)) (ht : ((λ (b : β), finset.image (λ (a : α), f a b) s) '' t).pairwise_disjoint id) :
s.card 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.

theorem finset.image₂_inter_union_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t t' : finset β} [decidable_eq α] [decidable_eq β] :
(s s') (t t') t s' t'
theorem finset.image₂_union_inter_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {f : α β γ} {s s' : finset α} {t t' : finset β} [decidable_eq α] [decidable_eq β] :
(s s') (t t') t s' t'
theorem finset.image₂_inter_union_subset {α : Type u_1} {β : Type u_3} [decidable_eq α] [decidable_eq β] {f : α α β} {s t : finset α} (hf : (a b : α), f a b = f b a) :
(s t) (s t) t
theorem finset.image₂_union_inter_subset {α : Type u_1} {β : Type u_3} [decidable_eq α] [decidable_eq β] {f : α α β} {s t : finset α} (hf : (a b : α), f a b = f b a) :
(s t) (s t) t
@[simp]
theorem set.to_finset_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] (f : α β γ) (s : set α) (t : set β) [fintype s] [fintype t] [fintype s t)] :
s t).to_finset =
theorem set.finite.to_finset_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} [decidable_eq γ] {s : set α} {t : set β} (f : α β γ) (hs : s.finite) (ht : t.finite) (hf : s t).finite := _) :