mathlib3 documentation

data.set.n_ary

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 α × β → γ.

Equations
Instances for set.image2
@[simp]
theorem set.mem_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} {t : set β} {c : γ} :
c set.image2 f s t (a : α) (b : β), a s b t f a b = c
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) :
f a b set.image2 f s t a s b t
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') :
theorem set.image2_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s s' : set α} {t : set β} (hs : s s') :
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.image2_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} {t : set β} {u : set γ} :
set.image2 f s t u (x : α), x s (y : β), y t f x y u
theorem set.image2_subset_iff_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} {t : set β} {u : set γ} :
set.image2 f s t u (a : α), a s (λ (b : β), f a b) '' t u
theorem set.image2_subset_iff_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} {t : set β} {u : set γ} :
set.image2 f s t u (b : β), b t (λ (a : α), f a b) '' s u
@[simp]
theorem set.image_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) {s : set α} {t : set β} :
(λ (x : α × β), f x.fst x.snd) '' s ×ˢ t = set.image2 f s t
@[simp]
theorem set.image_uncurry_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (s : set α) (t : set β) :
@[simp]
theorem set.image2_mk_eq_prod {α : Type u_1} {β : Type u_3} {s : set α} {t : set β} :
@[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 β} :
@[simp]
theorem set.image2_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} :
theorem set.nonempty.image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} {t : set β} :
@[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) :
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) :
@[simp]
theorem set.image2_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {s : set α} {t : set β} :
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 α × β × γ → δ.

Equations
@[simp]
theorem set.mem_image3 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {g : α β γ δ} {s : set α} {t : set β} {u : set γ} {d : δ} :
d set.image3 g s t u (a : α) (b : β) (c : γ), a s b t c u g a b c = d
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