N-ary images of sets #
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 the n-ary section of data.set.basic, to order.filter.n_ary and to
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
set.image2
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
(f : α → β → γ)
(s : set α)
(t : set β) :
set γ
The image of a binary function f : α → β → γ as a function set α → set β → set γ.
Mathematically this should be thought of as the image of the corresponding function α × β → γ.
Instances for ↥set.image2
theorem
set.mem_image2_of_mem
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{a : α}
{b : β}
(ha : a ∈ s)
(hb : b ∈ t) :
f a b ∈ set.image2 f s t
theorem
set.mem_image2_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{a : α}
{b : β}
(hf : function.injective2 f) :
theorem
set.image2_subset
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t t' : set β}
(hs : s ⊆ s')
(ht : t ⊆ t') :
set.image2 f s t ⊆ set.image2 f s' t'
image2 is monotone with respect to ⊆.
theorem
set.image2_subset_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t t' : set β}
(ht : t ⊆ t') :
set.image2 f s t ⊆ set.image2 f s t'
theorem
set.image2_subset_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t : set β}
(hs : s ⊆ s') :
set.image2 f s t ⊆ set.image2 f s' t
theorem
set.image_subset_image2_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{b : β}
(hb : b ∈ t) :
(λ (a : α), f a b) '' s ⊆ set.image2 f s t
theorem
set.image_subset_image2_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{a : α}
(ha : a ∈ s) :
f a '' t ⊆ set.image2 f s t
theorem
set.forall_image2_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{p : γ → Prop} :
(∀ (z : γ), z ∈ set.image2 f s t → p z) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (f x y)
@[simp]
theorem
set.image_uncurry_prod
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
(f : α → β → γ)
(s : set α)
(t : set β) :
function.uncurry f '' s ×ˢ t = set.image2 f s t
@[simp]
theorem
set.image2_mk_eq_prod
{α : Type u_1}
{β : Type u_3}
{s : set α}
{t : set β} :
set.image2 prod.mk s t = s ×ˢ t
@[simp]
theorem
set.image2_curry
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
(f : α × β → γ)
(s : set α)
(t : set β) :
set.image2 (λ (a : α) (b : β), f (a, b)) s t = f '' s ×ˢ t
theorem
set.image2_swap
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
(f : α → β → γ)
(s : set α)
(t : set β) :
set.image2 f s t = set.image2 (λ (a : β) (b : α), f b a) t s
theorem
set.image2_union_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t : set β} :
set.image2 f (s ∪ s') t = set.image2 f s t ∪ set.image2 f s' t
theorem
set.image2_union_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t t' : set β} :
set.image2 f s (t ∪ t') = set.image2 f s t ∪ set.image2 f s t'
theorem
set.image2_inter_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t : set β}
(hf : function.injective2 f) :
set.image2 f (s ∩ s') t = set.image2 f s t ∩ set.image2 f s' t
theorem
set.image2_inter_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t t' : set β}
(hf : function.injective2 f) :
set.image2 f s (t ∩ t') = set.image2 f s t ∩ set.image2 f s t'
@[simp]
theorem
set.image2_empty_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{t : set β} :
set.image2 f ∅ t = ∅
@[simp]
theorem
set.image2_empty_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α} :
set.image2 f s ∅ = ∅
theorem
set.nonempty.image2
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β} :
s.nonempty → t.nonempty → (set.image2 f s t).nonempty
@[simp]
theorem
set.image2_nonempty_iff
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β} :
theorem
set.nonempty.of_image2_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
(h : (set.image2 f s t).nonempty) :
s.nonempty
theorem
set.nonempty.of_image2_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
(h : (set.image2 f s t).nonempty) :
t.nonempty
theorem
set.image2_inter_subset_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t : set β} :
set.image2 f (s ∩ s') t ⊆ set.image2 f s t ∩ set.image2 f s' t
theorem
set.image2_inter_subset_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t t' : set β} :
set.image2 f s (t ∩ t') ⊆ set.image2 f s t ∩ set.image2 f s t'
@[simp]
theorem
set.image2_singleton_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{t : set β}
{a : α} :
set.image2 f {a} t = f a '' t
@[simp]
theorem
set.image2_singleton_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{b : β} :
set.image2 f s {b} = (λ (a : α), f a b) '' s
theorem
set.image2_singleton
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{a : α}
{b : β} :
set.image2 f {a} {b} = {f a b}
@[simp]
theorem
set.image2_insert_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{a : α} :
set.image2 f (has_insert.insert a s) t = (λ (b : β), f a b) '' t ∪ set.image2 f s t
@[simp]
theorem
set.image2_insert_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{b : β} :
set.image2 f s (has_insert.insert b t) = (λ (a : α), f a b) '' s ∪ set.image2 f s t
theorem
set.image2_congr
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f f' : α → β → γ}
{s : set α}
{t : set β}
(h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b) :
set.image2 f s t = set.image2 f' s t
theorem
set.image2_congr'
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f f' : α → β → γ}
{s : set α}
{t : set β}
(h : ∀ (a : α) (b : β), f a b = f' a b) :
set.image2 f s t = set.image2 f' s t
A common special case of image2_congr
def
set.image3
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
(g : α → β → γ → δ)
(s : set α)
(t : set β)
(u : set γ) :
set δ
The image of a ternary function f : α → β → γ → δ as a function
set α → set β → set γ → set δ. Mathematically this should be thought of as the image of the
corresponding function α × β × γ → δ.
theorem
set.image3_mono
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{g : α → β → γ → δ}
{s s' : set α}
{t t' : set β}
{u u' : set γ}
(hs : s ⊆ s')
(ht : t ⊆ t')
(hu : u ⊆ u') :
set.image3 g s t u ⊆ set.image3 g s' t' u'
theorem
set.image3_congr
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{g g' : α → β → γ → δ}
{s : set α}
{t : set β}
{u : set γ}
(h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → ∀ (c : γ), c ∈ u → g a b c = g' a b c) :
set.image3 g s t u = set.image3 g' s t u
theorem
set.image3_congr'
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{g g' : α → β → γ → δ}
{s : set α}
{t : set β}
{u : set γ}
(h : ∀ (a : α) (b : β) (c : γ), g a b c = g' a b c) :
set.image3 g s t u = set.image3 g' s t u
A common special case of image3_congr
theorem
set.image2_image2_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{s : set α}
{t : set β}
{u : set γ}
(f : δ → γ → ε)
(g : α → β → δ) :
set.image2 f (set.image2 g s t) u = set.image3 (λ (a : α) (b : β) (c : γ), f (g a b) c) s t u
theorem
set.image2_image2_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{s : set α}
{t : set β}
{u : set γ}
(f : α → δ → ε)
(g : β → γ → δ) :
set.image2 f s (set.image2 g t u) = set.image3 (λ (a : α) (b : β) (c : γ), f a (g b c)) s t u
theorem
set.image_image2
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
(f : α → β → γ)
(g : γ → δ) :
g '' set.image2 f s t = set.image2 (λ (a : α) (b : β), g (f a b)) s t
theorem
set.image2_image_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
(f : γ → β → δ)
(g : α → γ) :
set.image2 f (g '' s) t = set.image2 (λ (a : α) (b : β), f (g a) b) s t
theorem
set.image2_image_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
(f : α → γ → δ)
(g : β → γ) :
set.image2 f s (g '' t) = set.image2 (λ (a : α) (b : β), f a (g b)) s t
@[simp]
theorem
set.image2_left
{α : Type u_1}
{β : Type u_3}
{s : set α}
{t : set β}
(h : t.nonempty) :
set.image2 (λ (x : α) (y : β), x) s t = s
@[simp]
theorem
set.image2_right
{α : Type u_1}
{β : Type u_3}
{s : set α}
{t : set β}
(h : s.nonempty) :
set.image2 (λ (x : α) (y : β), y) s t = t
theorem
set.image2_assoc
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{ε' : Type u_10}
{s : set α}
{t : set β}
{u : set γ}
{f : δ → γ → ε}
{g : α → β → δ}
{f' : α → ε' → ε}
{g' : β → γ → ε'}
(h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) :
set.image2 f (set.image2 g s t) u = set.image2 f' s (set.image2 g' t u)
theorem
set.image2_comm
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : β → α → γ}
(h_comm : ∀ (a : α) (b : β), f a b = g b a) :
set.image2 f s t = set.image2 g t s
theorem
set.image2_left_comm
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{δ' : Type u_8}
{ε : Type u_9}
{s : set α}
{t : set β}
{u : set γ}
{f : α → δ → ε}
{g : β → γ → δ}
{f' : α → γ → δ'}
{g' : β → δ' → ε}
(h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) :
set.image2 f s (set.image2 g t u) = set.image2 g' t (set.image2 f' s u)
theorem
set.image2_right_comm
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{δ' : Type u_8}
{ε : Type u_9}
{s : set α}
{t : set β}
{u : set γ}
{f : δ → γ → ε}
{g : α → β → δ}
{f' : α → γ → δ'}
{g' : δ' → β → ε}
(h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) :
set.image2 f (set.image2 g s t) u = set.image2 g' (set.image2 f' s u) t
theorem
set.image2_image2_image2_comm
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{ε' : Type u_10}
{ζ : Type u_11}
{ζ' : Type u_12}
{ν : Type u_13}
{s : set α}
{t : set β}
{u : set γ}
{v : set δ}
{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)) :
set.image2 f (set.image2 g s t) (set.image2 h u v) = set.image2 f' (set.image2 g' s u) (set.image2 h' t v)
theorem
set.image_image2_distrib
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : γ → δ}
{f' : α' → β' → δ}
{g₁ : α → α'}
{g₂ : β → β'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) :
g '' set.image2 f s t = set.image2 f' (g₁ '' s) (g₂ '' t)
theorem
set.image_image2_distrib_left
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : γ → δ}
{f' : α' → β → δ}
{g' : α → α'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b) :
g '' set.image2 f s t = set.image2 f' (g' '' s) t
Symmetric statement to set.image2_image_left_comm.
theorem
set.image_image2_distrib_right
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : γ → δ}
{f' : α → β' → δ}
{g' : β → β'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)) :
g '' set.image2 f s t = set.image2 f' s (g' '' t)
Symmetric statement to set.image_image2_right_comm.
theorem
set.image2_image_left_comm
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
{f : α' → β → γ}
{g : α → α'}
{f' : α → β → δ}
{g' : δ → γ}
(h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)) :
set.image2 f (g '' s) t = g' '' set.image2 f' s t
Symmetric statement to set.image_image2_distrib_left.
theorem
set.image_image2_right_comm
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
{f : α → β' → γ}
{g : β → β'}
{f' : α → β → δ}
{g' : δ → γ}
(h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)) :
set.image2 f s (g '' t) = g' '' set.image2 f' s t
Symmetric statement to set.image_image2_distrib_right.
theorem
set.image2_distrib_subset_left
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{γ' : Type u_6}
{δ : Type u_7}
{ε : Type u_9}
{s : set α}
{t : set β}
{u : set γ}
{f : α → δ → ε}
{g : β → γ → δ}
{f₁ : α → β → β'}
{f₂ : α → γ → γ'}
{g' : β' → γ' → ε}
(h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) :
set.image2 f s (set.image2 g t u) ⊆ set.image2 g' (set.image2 f₁ s t) (set.image2 f₂ s u)
The other direction does not hold because of the s-s cross terms on the RHS.
theorem
set.image2_distrib_subset_right
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{s : set α}
{t : set β}
{u : set γ}
{f : δ → γ → ε}
{g : α → β → δ}
{f₁ : α → γ → α'}
{f₂ : β → γ → β'}
{g' : α' → β' → ε}
(h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) :
set.image2 f (set.image2 g s t) u ⊆ set.image2 g' (set.image2 f₁ s u) (set.image2 f₂ t u)
The other direction does not hold because of the u-u cross terms on the RHS.
theorem
set.image_image2_antidistrib
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : γ → δ}
{f' : β' → α' → δ}
{g₁ : β → β'}
{g₂ : α → α'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) :
g '' set.image2 f s t = set.image2 f' (g₁ '' t) (g₂ '' s)
theorem
set.image_image2_antidistrib_left
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : γ → δ}
{f' : β' → α → δ}
{g' : β → β'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a) :
g '' set.image2 f s t = set.image2 f' (g' '' t) s
Symmetric statement to set.image2_image_left_anticomm.
theorem
set.image_image2_antidistrib_right
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : set α}
{t : set β}
{g : γ → δ}
{f' : β → α' → δ}
{g' : α → α'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)) :
g '' set.image2 f s t = set.image2 f' t (g' '' s)
Symmetric statement to set.image_image2_right_anticomm.
theorem
set.image2_image_left_anticomm
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
{f : α' → β → γ}
{g : α → α'}
{f' : β → α → δ}
{g' : δ → γ}
(h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)) :
set.image2 f (g '' s) t = g' '' set.image2 f' t s
Symmetric statement to set.image_image2_antidistrib_left.
theorem
set.image_image2_right_anticomm
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{s : set α}
{t : set β}
{f : α → β' → γ}
{g : β → β'}
{f' : β → α → δ}
{g' : δ → γ}
(h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)) :
set.image2 f s (g '' t) = g' '' set.image2 f' t s
Symmetric statement to set.image_image2_antidistrib_right.
theorem
set.image2_left_identity
{α : Type u_1}
{β : Type u_3}
{f : α → β → β}
{a : α}
(h : ∀ (b : β), f a b = b)
(t : set β) :
set.image2 f {a} t = t
If a is a left identity for f : α → β → β, then {a} is a left identity for
set.image2 f.
theorem
set.image2_right_identity
{α : Type u_1}
{β : Type u_3}
{f : α → β → α}
{b : β}
(h : ∀ (a : α), f a b = a)
(s : set α) :
set.image2 f s {b} = s
If b is a right identity for f : α → β → α, then {b} is a right identity for
set.image2 f.
theorem
set.image2_inter_union_subset_union
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t t' : set β} :
set.image2 f (s ∩ s') (t ∪ t') ⊆ set.image2 f s t ∪ set.image2 f s' t'
theorem
set.image2_union_inter_subset_union
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s s' : set α}
{t t' : set β} :
set.image2 f (s ∪ s') (t ∩ t') ⊆ set.image2 f s t ∪ set.image2 f s' t'
theorem
set.image2_inter_union_subset
{α : Type u_1}
{β : Type u_3}
{f : α → α → β}
{s t : set α}
(hf : ∀ (a b : α), f a b = f b a) :
set.image2 f (s ∩ t) (s ∪ t) ⊆ set.image2 f s t
theorem
set.image2_union_inter_subset
{α : Type u_1}
{β : Type u_3}
{f : α → α → β}
{s t : set α}
(hf : ∀ (a b : α), f a b = f b a) :
set.image2 f (s ∪ t) (s ∩ t) ⊆ set.image2 f s t