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 the n-ary section of data.set.basic and to order.filter.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 β) :
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)
@[simp]
theorem
finset.mem_image₂
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
{s : finset α}
{t : finset β}
{c : γ} :
@[simp, norm_cast]
theorem
finset.coe_image₂
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
(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}
[decidable_eq γ]
(f : α → β → γ)
(s : finset α)
(t : finset β) :
theorem
finset.card_image₂_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
{s : finset α}
{t : finset β} :
theorem
finset.card_image₂
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
(hf : function.injective2 f)
(s : finset α)
(t : finset β) :
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 ∈ finset.image₂ f s 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) :
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') :
finset.image₂ f s t ⊆ finset.image₂ f 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') :
finset.image₂ f s t ⊆ finset.image₂ f s 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') :
finset.image₂ f s t ⊆ finset.image₂ f 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) :
(λ (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}
[decidable_eq γ]
{f : α → β → γ}
{s : finset α}
{t : finset β}
{a : α}
(ha : a ∈ s) :
f a '' ↑t ⊆ ↑(finset.image₂ f s 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 ∈ finset.image₂ f s 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 γ} :
@[simp]
theorem
finset.image₂_nonempty_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
{s : finset α}
{t : finset β} :
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) :
(finset.image₂ f 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 : (finset.image₂ f s t).nonempty) :
s.nonempty
theorem
finset.nonempty.of_image₂_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{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}
[decidable_eq γ]
{f : α → β → γ}
{t : finset β} :
finset.image₂ f ∅ t = ∅
@[simp]
theorem
finset.image₂_empty_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
{s : finset α} :
finset.image₂ f s ∅ = ∅
@[simp]
theorem
finset.image₂_eq_empty_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
{s : finset α}
{t : finset β} :
@[simp]
theorem
finset.image₂_singleton_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
{f : α → β → γ}
{t : finset β}
{a : α} :
finset.image₂ f {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 : β} :
finset.image₂ f s {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 : α} :
finset.image₂ f {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 : β} :
finset.image₂ f {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 α] :
finset.image₂ f (s ∪ s') t = finset.image₂ f s t ∪ finset.image₂ f 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 β] :
finset.image₂ f s (t ∪ t') = finset.image₂ f s t ∪ finset.image₂ f s 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 α] :
finset.image₂ f (s ∩ s') t ⊆ finset.image₂ f s t ∩ finset.image₂ f 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 β] :
finset.image₂ f s (t ∩ t') ⊆ finset.image₂ f s t ∩ finset.image₂ f 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 : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b) :
finset.image₂ f s t = finset.image₂ f' 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) :
finset.image₂ f s t = finset.image₂ f' 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 ⊆ set.image2 f 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)) :
(finset.image₂ f {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)) :
(finset.image₂ f 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)) :
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}
[decidable_eq γ]
{f : α → β → γ}
{b : β}
[decidable_eq α]
(s₁ s₂ : finset α)
(hf : function.injective (λ (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}
[decidable_eq γ]
{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}
[decidable_eq γ]
{f : α → β → γ}
(s : finset α)
{t : finset β}
(ht : t.nonempty)
(hf : ∀ (b : β), function.injective (λ (a : α), f a b)) :
s.card ≤ (finset.image₂ f 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) = finset.image₂ f s 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) = 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 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 : γ → δ) :
finset.image g (finset.image₂ f 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 : α → γ) :
finset.image₂ f (finset.image 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 : β → γ) :
finset.image₂ f s (finset.image g t) = finset.image₂ (λ (a : α) (b : β), f a (g b)) s t
theorem
finset.image₂_swap
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[decidable_eq γ]
(f : α → β → γ)
(s : finset α)
(t : finset β) :
finset.image₂ f s 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)) :
finset.image₂ f (finset.image₂ g s t) u = finset.image₂ f' s (finset.image₂ g' 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) :
finset.image₂ f s t = finset.image₂ g 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)) :
finset.image₂ f s (finset.image₂ g t u) = finset.image₂ g' t (finset.image₂ f' 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) :
finset.image₂ f (finset.image₂ g s t) u = finset.image₂ g' (finset.image₂ f' s u) t
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)) :
finset.image g (finset.image₂ f s t) = finset.image₂ f' (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) :
finset.image g (finset.image₂ f s t) = finset.image₂ f' (finset.image g' s) t
Symmetric of 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)) :
finset.image g (finset.image₂ f s t) = finset.image₂ f' s (finset.image g' t)
Symmetric of 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)) :
finset.image₂ f (finset.image g s) t = finset.image g' (finset.image₂ f' s t)
Symmetric of 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)) :
finset.image₂ f s (finset.image g t) = finset.image g' (finset.image₂ f' s t)
Symmetric of 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)) :
finset.image₂ f s (finset.image₂ g t u) ⊆ finset.image₂ g' (finset.image₂ f₁ s t) (finset.image₂ f₂ 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)) :
finset.image₂ f (finset.image₂ g s t) u ⊆ finset.image₂ g' (finset.image₂ f₁ s u) (finset.image₂ f₂ 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)) :
finset.image g (finset.image₂ f s t) = finset.image₂ f' (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) :
finset.image g (finset.image₂ f s t) = finset.image₂ f' (finset.image g' t) s
Symmetric of 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)) :
finset.image g (finset.image₂ f s t) = finset.image₂ f' t (finset.image g' s)
Symmetric of 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)) :
finset.image₂ f (finset.image g s) t = finset.image g' (finset.image₂ f' t s)
Symmetric of 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)) :
finset.image₂ f s (finset.image g t) = finset.image g' (finset.image₂ f' t s)
Symmetric of finset.image_image₂_antidistrib_right.