Documentation

Mathlib.Data.Finset.NAry

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.

def Finset.image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (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
Instances For
    @[simp]
    theorem Finset.mem_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {c : γ} :
    c Finset.image₂ f s t as, bt, f a b = c
    @[simp]
    theorem Finset.coe_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : αβγ) (s : Finset α) (t : Finset β) :
    (Finset.image₂ f s t) = Set.image2 f s t
    theorem Finset.card_image₂_le {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : αβγ) (s : Finset α) (t : Finset β) :
    (Finset.image₂ f s t).card s.card * t.card
    theorem Finset.card_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} :
    (Finset.image₂ f s t).card = s.card * t.card Set.InjOn (fun (x : α × β) => f x.1 x.2) (s ×ˢ t)
    theorem Finset.card_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} (hf : Function.Injective2 f) (s : Finset α) (t : Finset β) :
    (Finset.image₂ f s t).card = s.card * t.card
    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 Finset.image₂ f s t
    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 Finset.image₂ f s t a s b t
    theorem Finset.image₂_subset {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} (hs : s s') (ht : t t') :
    theorem Finset.image₂_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {t' : Finset β} (ht : t t') :
    theorem Finset.image₂_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} (hs : s s') :
    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) :
    Finset.image (fun (a : α) => f a b) s Finset.image₂ f s t
    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) :
    Finset.image (fun (b : β) => f a b) t Finset.image₂ f s t
    theorem Finset.forall_image₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {p : γProp} :
    (∀ zFinset.image₂ f s t, p z) xs, yt, p (f x y)
    @[simp]
    theorem Finset.image₂_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {u : Finset γ} :
    Finset.image₂ f s t u xs, yt, f x y u
    theorem Finset.image₂_subset_iff_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {u : Finset γ} :
    Finset.image₂ f s t u as, Finset.image (fun (b : β) => f a b) t u
    theorem Finset.image₂_subset_iff_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {u : Finset γ} :
    Finset.image₂ f s t u bt, Finset.image (fun (a : α) => f a b) s u
    @[simp]
    theorem Finset.image₂_nonempty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} :
    (Finset.image₂ f s t).Nonempty s.Nonempty t.Nonempty
    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
    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
    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
    @[simp]
    theorem Finset.image₂_empty_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {t : Finset β} :
    @[simp]
    theorem Finset.image₂_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} :
    @[simp]
    theorem Finset.image₂_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} :
    @[simp]
    theorem Finset.image₂_singleton_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {t : Finset β} {a : α} :
    Finset.image₂ f {a} t = Finset.image (fun (b : β) => f a b) t
    @[simp]
    theorem Finset.image₂_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {b : β} :
    Finset.image₂ f s {b} = Finset.image (fun (a : α) => f a b) s
    theorem Finset.image₂_singleton_left' {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {t : Finset β} {a : α} :
    theorem Finset.image₂_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {a : α} {b : β} :
    Finset.image₂ f {a} {b} = {f a b}
    theorem Finset.image₂_union_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} [DecidableEq α] :
    theorem Finset.image₂_union_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq β] :
    @[simp]
    theorem Finset.image₂_insert_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {a : α} [DecidableEq α] :
    Finset.image₂ f (insert a s) t = Finset.image (fun (b : β) => f a b) t Finset.image₂ f s t
    @[simp]
    theorem Finset.image₂_insert_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {b : β} [DecidableEq β] :
    Finset.image₂ f s (insert b t) = Finset.image (fun (a : α) => f a b) s Finset.image₂ f s t
    theorem Finset.image₂_inter_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} [DecidableEq α] (hf : Function.Injective2 f) :
    theorem Finset.image₂_inter_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq β] (hf : Function.Injective2 f) :
    theorem Finset.image₂_inter_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} [DecidableEq α] :
    theorem Finset.image₂_inter_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq β] :
    theorem Finset.image₂_congr {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {f' : αβγ} {s : Finset α} {t : Finset β} (h : as, bt, f a b = f' a b) :
    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) :

    A common special case of image₂_congr

    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)) :
    (Finset.image₂ f {a} t).card = t.card
    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) :
    (Finset.image₂ f s {b}).card = s.card
    theorem Finset.image₂_singleton_inter {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {a : α} [DecidableEq β] (t₁ : Finset β) (t₂ : Finset β) (hf : Function.Injective (f a)) :
    Finset.image₂ f {a} (t₁ t₂) = Finset.image₂ f {a} t₁ Finset.image₂ f {a} t₂
    theorem Finset.image₂_inter_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {b : β} [DecidableEq α] (s₁ : Finset α) (s₂ : Finset α) (hf : Function.Injective fun (a : α) => f a b) :
    Finset.image₂ f (s₁ s₂) {b} = Finset.image₂ f s₁ {b} Finset.image₂ f s₂ {b}
    theorem Finset.card_le_card_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} (t : Finset β) {s : Finset α} (hs : s.Nonempty) (hf : ∀ (a : α), Function.Injective (f a)) :
    t.card (Finset.image₂ f s t).card
    theorem Finset.card_le_card_image₂_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} (s : Finset α) {t : Finset β} (ht : t.Nonempty) (hf : ∀ (b : β), Function.Injective fun (a : α) => f a b) :
    s.card (Finset.image₂ f s t).card
    theorem Finset.biUnion_image_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} :
    (s.biUnion fun (a : α) => Finset.image (f a) t) = Finset.image₂ f s t
    theorem Finset.biUnion_image_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} :
    (t.biUnion fun (b : β) => Finset.image (fun (a : α) => f a b) s) = Finset.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.

    theorem Finset.image_image₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] (f : αβγ) (g : γδ) :
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ (fun (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} [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] (f : γβδ) (g : αγ) :
    Finset.image₂ f (Finset.image g s) t = Finset.image₂ (fun (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} [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] (f : αγδ) (g : βγ) :
    Finset.image₂ f s (Finset.image g t) = Finset.image₂ (fun (a : α) (b : β) => f a (g b)) s t
    @[simp]
    theorem Finset.image₂_mk_eq_product {α : Type u_1} {β : Type u_3} [DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset β) :
    Finset.image₂ Prod.mk s t = s ×ˢ t
    @[simp]
    theorem Finset.image₂_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : α × βγ) (s : Finset α) (t : Finset β) :
    @[simp]
    theorem Finset.image_uncurry_product {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : αβγ) (s : Finset α) (t : Finset β) :
    theorem Finset.image₂_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] (f : αβγ) (s : Finset α) (t : Finset β) :
    Finset.image₂ f s t = Finset.image₂ (fun (a : β) (b : α) => f b a) t s
    @[simp]
    theorem Finset.image₂_left {α : Type u_1} {β : Type u_3} {s : Finset α} {t : Finset β} [DecidableEq α] (h : t.Nonempty) :
    Finset.image₂ (fun (x : α) (x_1 : β) => x) s t = s
    @[simp]
    theorem Finset.image₂_right {α : Type u_1} {β : Type u_3} {s : Finset α} {t : Finset β} [DecidableEq β] (h : s.Nonempty) :
    Finset.image₂ (fun (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} [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)) :
    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) :
    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)) :
    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) :
    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)) :
    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)) :
    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) :

    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} [DecidableEq β'] [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γδ} {f' : αβ'δ} {g' : ββ'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)) :

    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} [DecidableEq α'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : α'βγ} {g : αα'} {f' : αβδ} {g' : δγ} (h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)) :

    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} [DecidableEq β'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : αβ'γ} {g : ββ'} {f' : αβδ} {g' : δγ} (h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)) :

    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} [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)) :

    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} [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)) :

    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} [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)) :
    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) :

    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} [DecidableEq α'] [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} [DecidableEq δ] {g : γδ} {f' : βα'δ} {g' : αα'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)) :

    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} [DecidableEq α'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : α'βγ} {g : αα'} {f' : βαδ} {g' : δγ} (h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)) :

    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} [DecidableEq β'] [DecidableEq γ] {s : Finset α} {t : Finset β} [DecidableEq δ] {f : αβ'γ} {g : ββ'} {f' : βαδ} {g' : δγ} (h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)) :

    Symmetric statement to Finset.image_image₂_antidistrib_right.

    theorem Finset.image₂_left_identity {α : Type u_1} {γ : Type u_5} [DecidableEq γ] {f : αγγ} {a : α} (h : ∀ (b : γ), f a b = b) (t : Finset γ) :
    Finset.image₂ f {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} [DecidableEq γ] {f : γβγ} {b : β} (h : ∀ (a : γ), f a b = a) (s : Finset γ) :
    Finset.image₂ f s {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} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} (hf : as, Function.Injective (f a)) (hs : ((fun (a : α) => Finset.image (f a) t) '' s).PairwiseDisjoint id) :
    t.card (Finset.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.

    theorem Finset.card_dvd_card_image₂_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {t : Finset β} (hf : bt, Function.Injective fun (a : α) => f a b) (ht : ((fun (b : β) => Finset.image (fun (a : α) => f a b) s) '' t).PairwiseDisjoint id) :
    s.card (Finset.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.

    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 Finset.image₂ f s' t'

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

    @[deprecated Finset.subset_set_image₂]
    theorem Finset.subset_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 Finset.image₂ f s' t'

    Alias of Finset.subset_set_image₂.


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

    theorem Finset.image₂_inter_union_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq α] [DecidableEq β] :
    theorem Finset.image₂_union_inter_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} [DecidableEq γ] {f : αβγ} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq α] [DecidableEq β] :
    theorem Finset.image₂_inter_union_subset {α : Type u_1} {β : Type u_3} [DecidableEq α] [DecidableEq β] {f : ααβ} {s : Finset α} {t : Finset α} (hf : ∀ (a b : α), f a b = f b a) :
    theorem Finset.image₂_union_inter_subset {α : Type u_1} {β : Type u_3} [DecidableEq α] [DecidableEq β] {f : ααβ} {s : Finset α} {t : Finset α} (hf : ∀ (a b : α), f a b = f b a) :
    @[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 : (Finset.image₂ f s t).Nonempty) :
    (Finset.image₂ f s t).sup' h g a xs, yt, g (f x y) a
    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 : (Finset.image₂ f s t).Nonempty) :
    (Finset.image₂ f s t).sup' h g = s.sup' fun (x : α) => t.sup' fun (x_1 : β) => g (f x x_1)
    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 : (Finset.image₂ f s t).Nonempty) :
    (Finset.image₂ f s t).sup' h g = t.sup' fun (y : β) => s.sup' fun (x : α) => g (f x y)
    @[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 : δ} :
    (Finset.image₂ f s t).sup g a xs, yt, g (f x y) a
    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 : γδ) :
    (Finset.image₂ f s t).sup g = s.sup fun (x : α) => t.sup fun (x_1 : β) => g (f x x_1)
    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 : γδ) :
    (Finset.image₂ f s t).sup g = t.sup fun (y : β) => s.sup fun (x : α) => g (f x y)
    @[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 : (Finset.image₂ f s t).Nonempty) :
    a (Finset.image₂ f s t).inf' h g xs, yt, a g (f x y)
    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 : (Finset.image₂ f s t).Nonempty) :
    (Finset.image₂ f s t).inf' h g = s.inf' fun (x : α) => t.inf' fun (x_1 : β) => g (f x x_1)
    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 : (Finset.image₂ f s t).Nonempty) :
    (Finset.image₂ f s t).inf' h g = t.inf' fun (y : β) => s.inf' fun (x : α) => g (f x y)
    @[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 (Finset.image₂ f s t).inf g xs, yt, a g (f x y)
    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 : γδ) :
    (Finset.image₂ f s t).inf g = s.inf fun (x : α) => t.inf (g f x)
    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 : γδ) :
    (Finset.image₂ f s t).inf g = t.inf fun (y : β) => s.inf fun (x : α) => g (f x y)
    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)) :
    (Fintype.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)) (Fintype.piFinset s) (Fintype.piFinset t)
    @[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 (Set.image2 f s t)] :
    (Set.image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset
    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 : optParam (Set.image2 f s t).Finite ) :
    Set.Finite.toFinset hf = Finset.image₂ f hs.toFinset ht.toFinset