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 β)
:
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
@[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 ↔ ∃ a ∈ s, ∃ b ∈ t, 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 β}
:
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)
:
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')
:
Finset.image₂ f s t ⊆ Finset.image₂ f s' 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')
:
Finset.image₂ f s t ⊆ Finset.image₂ f s 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')
:
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}
[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}
:
(∀ z ∈ Finset.image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, 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 ↔ ∀ x ∈ s, ∀ y ∈ t, 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 ↔ ∀ a ∈ s, 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 ↔ ∀ b ∈ t, 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 β}
:
Finset.image₂ f ∅ t = ∅
@[simp]
theorem
Finset.image₂_empty_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[DecidableEq γ]
{f : α → β → γ}
{s : Finset α}
:
Finset.image₂ f s ∅ = ∅
@[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 : α}
:
Finset.image₂ f {a} t = Finset.image (f a) t
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 α]
:
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}
[DecidableEq γ]
{f : α → β → γ}
{s : Finset α}
{t : Finset β}
{t' : Finset β}
[DecidableEq β]
:
Finset.image₂ f s (t ∪ t') = Finset.image₂ f s t ∪ Finset.image₂ f s t'
@[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)
:
Finset.image₂ f (s ∩ s') t = Finset.image₂ f s t ∩ Finset.image₂ f s' t
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)
:
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}
[DecidableEq γ]
{f : α → β → γ}
{s : Finset α}
{s' : Finset α}
{t : Finset β}
[DecidableEq α]
:
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}
[DecidableEq γ]
{f : α → β → γ}
{s : Finset α}
{t : Finset β}
{t' : Finset β}
[DecidableEq β]
:
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}
[DecidableEq γ]
{f : α → β → γ}
{f' : α → β → γ}
{s : Finset α}
{t : Finset β}
(h : ∀ a ∈ s, ∀ 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}
[DecidableEq γ]
{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.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 β)
:
Finset.image₂ (Function.curry f) s t = Finset.image f (s ×ˢ t)
@[simp]
theorem
Finset.image_uncurry_product
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[DecidableEq γ]
(f : α → β → γ)
(s : Finset α)
(t : Finset β)
:
Finset.image (Function.uncurry f) (s ×ˢ t) = Finset.image₂ f s t
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))
:
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}
[DecidableEq γ]
{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}
[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))
:
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}
[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)
:
Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ g' (Finset.image₂ f' 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}
[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))
:
Finset.image₂ f (Finset.image₂ g s t) (Finset.image₂ h u v) = Finset.image₂ f' (Finset.image₂ g' s u) (Finset.image₂ h' 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}
[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))
:
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}
[DecidableEq α']
[DecidableEq γ]
{f : α → β → γ}
{s : Finset α}
{t : Finset β}
[DecidableEq δ]
{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 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))
:
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' 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}
[DecidableEq α']
[DecidableEq γ]
{s : Finset α}
{t : Finset β}
[DecidableEq δ]
{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 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))
:
Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' 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}
[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))
:
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}
[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))
:
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}
[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))
:
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}
[DecidableEq β']
[DecidableEq γ]
{f : α → β → γ}
{s : Finset α}
{t : Finset β}
[DecidableEq δ]
{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 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))
:
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' 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}
[DecidableEq α']
[DecidableEq γ]
{s : Finset α}
{t : Finset β}
[DecidableEq δ]
{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 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))
:
Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' t s)
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 : ∀ a ∈ s, 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 : ∀ b ∈ t, 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_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)
:
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 β]
:
Finset.image₂ f (s ∩ s') (t ∪ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
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 β]
:
Finset.image₂ f (s ∪ s') (t ∩ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
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)
:
Finset.image₂ f (s ∩ t) (s ∪ t) ⊆ Finset.image₂ f s t
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)
:
Finset.image₂ f (s ∪ t) (s ∩ t) ⊆ Finset.image₂ f s t
@[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 ↔ ∀ x ∈ s, ∀ y ∈ t, 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 ↔ ∀ x ∈ s, ∀ y ∈ t, 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 ↔ ∀ x ∈ s, ∀ y ∈ t, 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 ↔ ∀ x ∈ s, ∀ y ∈ t, 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