# Documentation

Mathlib.Data.Set.Image

# Images and preimages of sets #

## Main definitions #

• preimage f t : Set α : the preimage f⁻¹(t) (written f ⁻¹' t⁻¹' t in Lean) of a subset of β.

• range f : Set β : the image of univ under f. Also works for {p : Prop} (f : p → α)→ α) (unlike image)

## Notation #

• f ⁻¹' t⁻¹' t for Set.preimage f t

• f '' s for Set.image f s

## Tags #

set, sets, image, preimage, pre-image, range

### Inverse image #

def Set.preimage {α : Type u} {β : Type v} (f : αβ) (s : Set β) :
Set α

The preimage of s : Set β by f : α → β→ β, written f ⁻¹' s⁻¹' s, is the set of x : α such that f x ∈ s∈ s.

Equations

f ⁻¹' t⁻¹' t denotes the preimage of t : Set β under the function f : α → β→ β.

Equations
@[simp]
theorem Set.preimage_empty {α : Type u_1} {β : Type u_2} {f : αβ} :
@[simp]
theorem Set.mem_preimage {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} {a : α} :
a f ⁻¹' s f a s
theorem Set.preimage_congr {α : Type u_2} {β : Type u_1} {f : αβ} {g : αβ} {s : Set β} (h : ∀ (x : α), f x = g x) :
f ⁻¹' s = g ⁻¹' s
theorem Set.preimage_mono {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} {t : Set β} (h : s t) :
f ⁻¹' s f ⁻¹' t
@[simp]
theorem Set.preimage_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
f ⁻¹' Set.univ = Set.univ
theorem Set.subset_preimage_univ {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
s f ⁻¹' Set.univ
@[simp]
theorem Set.preimage_inter {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} {t : Set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem Set.preimage_union {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} {t : Set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem Set.preimage_compl {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
@[simp]
theorem Set.preimage_diff {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) (t : Set β) :
f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
@[simp]
theorem Set.preimage_ite {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) (t₁ : Set β) (t₂ : Set β) :
f ⁻¹' Set.ite s t₁ t₂ = Set.ite (f ⁻¹' s) (f ⁻¹' t₁) (f ⁻¹' t₂)
@[simp]
theorem Set.preimage_setOf_eq {α : Type u_2} {β : Type u_1} {p : αProp} {f : βα} :
f ⁻¹' { a | p a } = { a | p (f a) }
@[simp]
theorem Set.preimage_id_eq {α : Type u_1} :
= id
theorem Set.preimage_id {α : Type u_1} {s : Set α} :
id ⁻¹' s = s
@[simp]
theorem Set.preimage_id' {α : Type u_1} {s : Set α} :
(fun x => x) ⁻¹' s = s
@[simp]
theorem Set.preimage_const_of_mem {α : Type u_2} {β : Type u_1} {b : β} {s : Set β} (h : b s) :
(fun x => b) ⁻¹' s = Set.univ
@[simp]
theorem Set.preimage_const_of_not_mem {α : Type u_2} {β : Type u_1} {b : β} {s : Set β} (h : ¬b s) :
(fun x => b) ⁻¹' s =
theorem Set.preimage_const {α : Type u_2} {β : Type u_1} (b : β) (s : Set β) [inst : Decidable (b s)] :
(fun x => b) ⁻¹' s = if b s then Set.univ else
theorem Set.preimage_comp {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβ} {g : βγ} {s : Set γ} :
g f ⁻¹' s = f ⁻¹' (g ⁻¹' s)
theorem Set.preimage_comp_eq {α : Type u_1} {β : Type u_3} {γ : Type u_2} {f : αβ} {g : βγ} :
@[simp]
theorem Set.preimage_iterate_eq {α : Type u_1} {f : αα} {n : } :
theorem Set.preimage_preimage {α : Type u_2} {β : Type u_3} {γ : Type u_1} {g : βγ} {f : αβ} {s : Set γ} :
f ⁻¹' (g ⁻¹' s) = (fun x => g (f x)) ⁻¹' s
theorem Set.eq_preimage_subtype_val_iff {α : Type u_1} {p : αProp} {s : Set ()} {t : Set α} :
s = Subtype.val ⁻¹' t ∀ (x : α) (h : p x), { val := x, property := h } s x t
theorem Set.nonempty_of_nonempty_preimage {α : Type u_2} {β : Type u_1} {s : Set β} {f : αβ} (hf : Set.Nonempty (f ⁻¹' s)) :
theorem Set.preimage_subtype_coe_eq_compl {α : Type u_1} {s : Set α} {u : Set α} {v : Set α} (hsuv : s u v) (H : s (u v) = ) :
Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)

### Image of a set under a function #

f '' s denotes the image of s : Set α under the function f : α → β→ β.

Equations
theorem Set.mem_image_iff_bex {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {y : β} :
y f '' s x x_1, f x = y
@[simp]
theorem Set.mem_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (y : β) :
y f '' s x, x s f x = y
theorem Set.image_eta {α : Type u_2} {β : Type u_1} {s : Set α} (f : αβ) :
f '' s = (fun x => f x) '' s
theorem Set.mem_image_of_mem {α : Type u_1} {β : Type u_2} (f : αβ) {x : α} {a : Set α} (h : x a) :
f x f '' a
theorem Function.Injective.mem_set_image {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {s : Set α} {a : α} :
f a f '' s a s
theorem Set.ball_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {p : βProp} :
((y : β) → y f '' sp y) (x : α) → x sp (f x)
theorem Set.ball_image_of_ball {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {p : βProp} (h : (x : α) → x sp (f x)) (y : β) :
y f '' sp y
theorem Set.bex_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {p : βProp} :
(y, y f '' s p y) x, x s p (f x)
theorem Set.mem_image_elim {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {C : βProp} (h : (x : α) → x sC (f x)) {y : β} :
y f '' sC y
theorem Set.mem_image_elim_on {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {C : βProp} {y : β} (h_y : y f '' s) (h : (x : α) → x sC (f x)) :
C y
theorem Set.image_congr {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {s : Set α} (h : ∀ (a : α), a sf a = g a) :
f '' s = g '' s
theorem Set.image_congr' {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {s : Set α} (h : ∀ (x : α), f x = g x) :
f '' s = g '' s

A common special case of image_congr

theorem Set.image_comp {α : Type u_1} {β : Type u_3} {γ : Type u_2} (f : βγ) (g : αβ) (a : Set α) :
f g '' a = f '' (g '' a)
theorem Set.image_image {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : βγ) (f : αβ) (s : Set α) :
g '' (f '' s) = (fun x => g (f x)) '' s

A variant of image_comp, useful for rewriting

theorem Set.image_comm {α : Type u_4} {β : Type u_3} {γ : Type u_2} {s : Set α} {β' : Type u_1} {f : βγ} {g : αβ} {f' : αβ'} {g' : β'γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) :
f '' (g '' s) = g' '' (f' '' s)
theorem Function.Semiconj.set_image {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {gb : ββ} (h : Function.Semiconj f ga gb) :
theorem Function.Commute.set_image {α : Type u_1} {f : αα} {g : αα} (h : ) :
theorem Set.image_subset {α : Type u_1} {β : Type u_2} {a : Set α} {b : Set α} (f : αβ) (h : a b) :
f '' a f '' b

Image is monotone with respect to ⊆⊆. See Set.monotone_image for the statement in terms of ≤≤.

theorem Set.monotone_image {α : Type u_1} {β : Type u_2} {f : αβ} :

Set.image is monotone. See Set.image_subset for the statement in terms of ⊆⊆.

theorem Set.image_union {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set α) :
f '' (s t) = f '' s f '' t
@[simp]
theorem Set.image_empty {α : Type u_2} {β : Type u_1} (f : αβ) :
theorem Set.image_inter_subset {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set α) :
f '' (s t) f '' s f '' t
theorem Set.image_inter_on {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} (h : ∀ (x : α), x t∀ (y : α), y sf x = f yx = y) :
f '' (s t) = f '' s f '' t
theorem Set.image_inter {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} (H : ) :
f '' (s t) = f '' s f '' t
theorem Set.image_univ_of_surjective {β : Type u_2} {ι : Type u_1} {f : ιβ} (H : ) :
f '' Set.univ = Set.univ
@[simp]
theorem Set.image_singleton {α : Type u_2} {β : Type u_1} {f : αβ} {a : α} :
f '' {a} = {f a}
@[simp]
theorem Set.Nonempty.image_const {α : Type u_1} {β : Type u_2} {s : Set α} (hs : ) (a : β) :
(fun x => a) '' s = {a}
@[simp]
theorem Set.image_eq_empty {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
f '' s = s =
theorem Set.preimage_compl_eq_image_compl {α : Type u_1} [inst : ] (S : Set α) :
compl ⁻¹' S = compl '' S
theorem Set.mem_compl_image {α : Type u_1} [inst : ] (t : α) (S : Set α) :
t compl '' S t S
@[simp]
theorem Set.image_id' {α : Type u_1} (s : Set α) :
(fun x => x) '' s = s

A variant of image_id

theorem Set.image_id {α : Type u_1} (s : Set α) :
id '' s = s
theorem Set.compl_compl_image {α : Type u_1} [inst : ] (S : Set α) :
compl '' (compl '' S) = S
theorem Set.image_insert_eq {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {s : Set α} :
f '' insert a s = insert (f a) (f '' s)
theorem Set.image_pair {α : Type u_2} {β : Type u_1} (f : αβ) (a : α) (b : α) :
f '' {a, b} = {f a, f b}
theorem Set.image_subset_preimage_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (I : ) (s : Set α) :
f '' s g ⁻¹' s
theorem Set.preimage_subset_image_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (I : ) (s : Set β) :
f ⁻¹' s g '' s
theorem Set.image_eq_preimage_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h₁ : ) (h₂ : ) :
theorem Set.mem_image_iff_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} {b : β} {s : Set α} (h₁ : ) (h₂ : ) :
b f '' s g b s
theorem Set.image_compl_subset {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} (H : ) :
f '' s (f '' s)
theorem Set.subset_image_compl {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} (H : ) :
(f '' s) f '' s
theorem Set.image_compl_eq {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} (H : ) :
f '' s = (f '' s)
theorem Set.subset_image_diff {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set α) :
f '' s \ f '' t f '' (s \ t)
theorem Set.subset_image_symm_diff {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set α} {t : Set α} :
(f '' s) (f '' t) f '' s t
theorem Set.image_diff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set α) (t : Set α) :
f '' (s \ t) = f '' s \ f '' t
theorem Set.image_symm_diff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set α) (t : Set α) :
f '' s t = (f '' s) (f '' t)
theorem Set.Nonempty.image {α : Type u_1} {β : Type u_2} (f : αβ) {s : Set α} :
Set.Nonempty (f '' s)
theorem Set.Nonempty.of_image {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
Set.Nonempty (f '' s)
@[simp]
theorem Set.nonempty_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
theorem Set.Nonempty.preimage {α : Type u_2} {β : Type u_1} {s : Set β} (hs : ) {f : αβ} (hf : ) :
instance Set.instNonemptyElemImage {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) [inst : Nonempty s] :
Nonempty ↑(f '' s)
Equations
@[simp]
theorem Set.image_subset_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} :
f '' s t s f ⁻¹' t

image and preimage are a Galois connection

theorem Set.image_preimage_subset {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) :
f '' (f ⁻¹' s) s
theorem Set.subset_preimage_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
s f ⁻¹' (f '' s)
theorem Set.preimage_image_eq {α : Type u_1} {β : Type u_2} {f : αβ} (s : Set α) (h : ) :
f ⁻¹' (f '' s) = s
theorem Set.image_preimage_eq {α : Type u_2} {β : Type u_1} {f : αβ} (s : Set β) (h : ) :
f '' (f ⁻¹' s) = s
theorem Set.preimage_eq_preimage {α : Type u_2} {β : Type u_1} {s : Set α} {t : Set α} {f : βα} (hf : ) :
f ⁻¹' s = f ⁻¹' t s = t
theorem Set.image_inter_preimage {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :
f '' (s f ⁻¹' t) = f '' s t
theorem Set.image_preimage_inter {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :
f '' (f ⁻¹' t s) = t f '' s
@[simp]
theorem Set.image_inter_nonempty_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set β} :
theorem Set.image_diff_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set β} :
f '' (s \ f ⁻¹' t) = f '' s \ t
theorem Set.compl_image {α : Type u_1} :
theorem Set.compl_image_set_of {α : Type u_1} {p : Set αProp} :
compl '' { s | p s } = { s | p (s) }
theorem Set.inter_preimage_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : αβ) :
s f ⁻¹' t f ⁻¹' (f '' s t)
theorem Set.union_preimage_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : αβ) :
s f ⁻¹' t f ⁻¹' (f '' s t)
theorem Set.subset_image_union {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :
f '' (s f ⁻¹' t) f '' s t
theorem Set.preimage_subset_iff {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {f : αβ} :
f ⁻¹' B A ∀ (a : α), f a Ba A
theorem Set.image_eq_image {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : αβ} (hf : ) :
f '' s = f '' t s = t
theorem Set.image_subset_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : αβ} (hf : ) :
f '' s f '' t s t
theorem Set.prod_quotient_preimage_eq_image {α : Type u_1} {β : Type u_2} [s : ] (g : β) {h : αβ} (Hh : h = g Quotient.mk'') (r : Set (β × β)) :
{ x | (g x.fst, g x.snd) r } = (fun a => (Quotient.mk s a.fst, Quotient.mk s a.snd)) '' ((fun a => (h a.fst, h a.snd)) ⁻¹' r)
theorem Set.exists_image_iff {α : Type u_1} {β : Type u_2} (f : αβ) (x : Set α) (P : βProp) :
(a, P a) a, P (f a)
def Set.imageFactorization {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
s↑(f '' s)

Restriction of f to s factors through s.imageFactorization f : s → f '' s→ f '' s.

Equations
• = { val := f p, property := (_ : f p f '' s) }
theorem Set.imageFactorization_eq {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
Subtype.val = f Subtype.val
theorem Set.surjective_onto_image {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
theorem Set.image_perm {α : Type u_1} {s : Set α} {σ : } (hs : { a | σ a a } s) :
σ '' s = s

If the only elements outside s are those left fixed by σ, then mapping by σ has no effect.

### Lemmas about the powerset and image. #

theorem Set.powerset_insert {α : Type u_1} (s : Set α) (a : α) :

The powerset of {a} ∪ s∪ s is 𝒫 s together with {a} ∪ t∪ t for each t ∈ 𝒫 s∈ 𝒫 s.

### Lemmas about range of a function. #

def Set.range {α : Type u_1} {ι : Sort u_2} (f : ια) :
Set α

Range of a function.

This function is more flexible than f '' univ, as the image requires that the domain is in Type and not an arbitrary Sort.

Equations
• = { x | y, f y = x }
@[simp]
theorem Set.mem_range {α : Type u_1} {ι : Sort u_2} {f : ια} {x : α} :
x y, f y = x
theorem Set.mem_range_self {α : Type u_1} {ι : Sort u_2} {f : ια} (i : ι) :
f i
theorem Set.forall_range_iff {α : Type u_1} {ι : Sort u_2} {f : ια} {p : αProp} :
((a : α) → a p a) (i : ι) → p (f i)
theorem Set.forall_subtype_range_iff {α : Type u_1} {ι : Sort u_2} {f : ια} {p : ↑()Prop} :
((a : ↑()) → p a) (i : ι) → p { val := f i, property := (_ : f i ) }
theorem Set.exists_range_iff {α : Type u_1} {ι : Sort u_2} {f : ια} {p : αProp} :
(a, a p a) i, p (f i)
theorem Set.exists_range_iff' {α : Type u_1} {ι : Sort u_2} {f : ια} {p : αProp} :
(a, a p a) i, p (f i)
theorem Set.exists_subtype_range_iff {α : Type u_1} {ι : Sort u_2} {f : ια} {p : ↑()Prop} :
(a, p a) i, p { val := f i, property := (_ : f i ) }
theorem Set.range_iff_surjective {α : Type u_1} {ι : Sort u_2} {f : ια} :
= Set.univ
theorem Function.Surjective.range_eq {α : Type u_1} {ι : Sort u_2} {f : ια} :
= Set.univ

Alias of the reverse direction of Set.range_iff_surjective.

@[simp]
theorem Set.image_univ {α : Type u_2} {β : Type u_1} {f : αβ} :
f '' Set.univ =
theorem Set.image_subset_range {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
f '' s
theorem Set.mem_range_of_mem_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) {x : β} (h : x f '' s) :
x
theorem Nat.mem_range_succ (i : ) :
0 < i
theorem Set.Nonempty.preimage' {α : Type u_2} {β : Type u_1} {s : Set β} (hs : ) {f : αβ} (hf : s ) :
theorem Set.range_comp {α : Type u_3} {β : Type u_1} {ι : Sort u_2} (g : αβ) (f : ια) :
Set.range (g f) = g ''
theorem Set.range_subset_iff {α : Type u_1} {ι : Sort u_2} {f : ια} {s : Set α} :
s ∀ (y : ι), f y s
theorem Set.range_eq_iff {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) :
= s (∀ (a : α), f a s) ∀ (b : β), b sa, f a = b
theorem Set.range_comp_subset_range {α : Type u_2} {β : Type u_3} {γ : Type u_1} (f : αβ) (g : βγ) :
theorem Set.range_nonempty_iff_nonempty {α : Type u_1} {ι : Sort u_2} {f : ια} :
theorem Set.range_nonempty {α : Type u_2} {ι : Sort u_1} [h : ] (f : ια) :
@[simp]
theorem Set.range_eq_empty_iff {α : Type u_1} {ι : Sort u_2} {f : ια} :
theorem Set.range_eq_empty {α : Type u_2} {ι : Sort u_1} [inst : ] (f : ια) :
instance Set.instNonemptyElemRange {α : Type u_1} {ι : Sort u_2} [inst : ] (f : ια) :
Nonempty ↑()
Equations
@[simp]
theorem Set.image_union_image_compl_eq_range {α : Type u_2} {β : Type u_1} {s : Set α} (f : αβ) :
f '' s f '' s =
theorem Set.insert_image_compl_eq_range {α : Type u_2} {β : Type u_1} (f : αβ) (x : α) :
insert (f x) (f '' {x}) =
theorem Set.image_preimage_eq_inter_range {α : Type u_2} {β : Type u_1} {f : αβ} {t : Set β} :
f '' (f ⁻¹' t) = t
theorem Set.image_preimage_eq_of_subset {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} (hs : s ) :
f '' (f ⁻¹' s) = s
theorem Set.image_preimage_eq_iff {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
f '' (f ⁻¹' s) = s s
theorem Set.subset_range_iff_exists_image_eq {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
s t, f '' t = s
theorem Set.range_image {α : Type u_2} {β : Type u_1} (f : αβ) :
=
@[simp]
theorem Set.exists_subset_range_and_iff {α : Type u_2} {β : Type u_1} {f : αβ} {p : Set βProp} :
(s, s p s) s, p (f '' s)
theorem Set.exists_subset_range_iff {α : Type u_2} {β : Type u_1} {f : αβ} {p : Set βProp} :
(s x, p s) s, p (f '' s)
theorem Set.forall_subset_range_iff {α : Type u_2} {β : Type u_1} {f : αβ} {p : Set βProp} :
((s : Set β) → s p s) (s : Set α) → p (f '' s)
theorem Set.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : βα} (hs : s ) :
f ⁻¹' s f ⁻¹' t s t
theorem Set.preimage_eq_preimage' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : βα} (hs : s ) (ht : t ) :
f ⁻¹' s = f ⁻¹' t s = t
theorem Set.preimage_inter_range {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
f ⁻¹' (s ) = f ⁻¹' s
theorem Set.preimage_range_inter {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
f ⁻¹' ( s) = f ⁻¹' s
theorem Set.preimage_image_preimage {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
@[simp]
theorem Set.range_id {α : Type u_1} :
= Set.univ
@[simp]
theorem Set.range_id' {α : Type u_1} :
(Set.range fun x => x) = Set.univ
@[simp]
theorem Prod.range_fst {α : Type u_2} {β : Type u_1} [inst : ] :
Set.range Prod.fst = Set.univ
@[simp]
theorem Prod.range_snd {α : Type u_1} {β : Type u_2} [inst : ] :
Set.range Prod.snd = Set.univ
@[simp]
theorem Set.range_eval {ι : Type u_1} {α : ιType u_2} [inst : ∀ (i : ι), Nonempty (α i)] (i : ι) :
= Set.univ
theorem Set.range_inl {α : Type u_1} {β : Type u_2} :
Set.range Sum.inl = { x | }
theorem Set.range_inr {α : Type u_1} {β : Type u_2} :
Set.range Sum.inr = { x | }
theorem Set.isCompl_range_inl_range_inr {α : Type u_1} {β : Type u_2} :
IsCompl (Set.range Sum.inl) (Set.range Sum.inr)
@[simp]
theorem Set.range_inl_union_range_inr {α : Type u_1} {β : Type u_2} :
Set.range Sum.inl Set.range Sum.inr = Set.univ
@[simp]
theorem Set.range_inl_inter_range_inr {α : Type u_1} {β : Type u_2} :
Set.range Sum.inl Set.range Sum.inr =
@[simp]
theorem Set.range_inr_union_range_inl {α : Type u_1} {β : Type u_2} :
Set.range Sum.inr Set.range Sum.inl = Set.univ
@[simp]
theorem Set.range_inr_inter_range_inl {α : Type u_1} {β : Type u_2} :
Set.range Sum.inr Set.range Sum.inl =
@[simp]
theorem Set.preimage_inl_image_inr {α : Type u_2} {β : Type u_1} (s : Set β) :
Sum.inl ⁻¹' (Sum.inr '' s) =
@[simp]
theorem Set.preimage_inr_image_inl {α : Type u_1} {β : Type u_2} (s : Set α) :
Sum.inr ⁻¹' (Sum.inl '' s) =
@[simp]
theorem Set.preimage_inl_range_inr {α : Type u_1} {β : Type u_2} :
Sum.inl ⁻¹' Set.range Sum.inr =
@[simp]
theorem Set.preimage_inr_range_inl {α : Type u_2} {β : Type u_1} :
Sum.inr ⁻¹' Set.range Sum.inl =
@[simp]
theorem Set.compl_range_inl {α : Type u_1} {β : Type u_2} :
Set.range Sum.inl = Set.range Sum.inr
@[simp]
theorem Set.compl_range_inr {α : Type u_1} {β : Type u_2} :
Set.range Sum.inr = Set.range Sum.inl
theorem Set.image_preimage_inl_union_image_preimage_inr {α : Type u_2} {β : Type u_1} (s : Set (α β)) :
Sum.inl '' (Sum.inl ⁻¹' s) Sum.inr '' (Sum.inr ⁻¹' s) = s
@[simp]
theorem Set.range_quot_mk {α : Type u_1} (r : ααProp) :
Set.range () = Set.univ
@[simp]
theorem Set.range_quot_lift {α : Type u_1} {ι : Sort u_2} {f : ια} {r : ιιProp} (hf : ∀ (x y : ι), r x yf x = f y) :
@[simp]
theorem Set.range_quotient_mk {α : Type u_1} [sa : ] :
(Set.range fun x => Quotient.mk sa x) = Set.univ
@[simp]
theorem Set.range_quotient_lift {α : Type u_2} {ι : Sort u_1} {f : ια} [s : ] (hf : ∀ (a b : ι), a bf a = f b) :
@[simp]
theorem Set.range_quotient_mk' {α : Type u_1} {s : } :
Set.range Quotient.mk' = Set.univ
@[simp]
theorem Set.range_quotient_lift_on' {α : Type u_2} {ι : Sort u_1} {f : ια} {s : } (hf : ∀ (a b : ι), Setoid.r a bf a = f b) :
(Set.range fun x => Quotient.liftOn' x f hf) =
instance Set.canLift {α : Type u_1} {β : Type u_2} (c : βα) (p : αProp) [inst : CanLift α β c p] :
CanLift (Set α) (Set β) ((fun x x_1 => x '' x_1) c) fun s => (x : α) → x sp x
Equations
• = { prf := (_ : ∀ (x : Set α), ((x_1 : α) → x_1 xp x_1) → t, c '' t = x) }
theorem Set.range_const_subset {α : Type u_1} {ι : Sort u_2} {c : α} :
(Set.range fun x => c) {c}
@[simp]
theorem Set.range_const {α : Type u_2} {ι : Sort u_1} [inst : ] {c : α} :
(Set.range fun x => c) = {c}
theorem Set.range_subtype_map {α : Type u_2} {β : Type u_1} {p : αProp} {q : βProp} (f : αβ) (h : (x : α) → p xq (f x)) :
Set.range () = Subtype.val ⁻¹' (f '' { x | p x })
theorem Set.image_swap_eq_preimage_swap {α : Type u_1} {β : Type u_2} :
Set.image Prod.swap = Set.preimage Prod.swap
theorem Set.preimage_singleton_nonempty {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} :
theorem Set.preimage_singleton_eq_empty {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} :
f ⁻¹' {y} = ¬y
theorem Set.range_subset_singleton {α : Type u_1} {ι : Sort u_2} {f : ια} {x : α} :
{x} f =
theorem Set.image_compl_preimage {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :
f '' (f ⁻¹' s) = \ s
def Set.rangeFactorization {β : Type u_1} {ι : Sort u_2} (f : ιβ) :
ι↑()

Any map f : ι → β→ β factors through a map rangeFactorization f : ι → range f→ range f.

Equations
• = { val := f i, property := (_ : f i ) }
theorem Set.rangeFactorization_eq {β : Type u_1} {ι : Sort u_2} {f : ιβ} :
Subtype.val = f
@[simp]
theorem Set.rangeFactorization_coe {β : Type u_1} {ι : Sort u_2} (f : ιβ) (a : ι) :
↑() = f a
@[simp]
theorem Set.coe_comp_rangeFactorization {β : Type u_1} {ι : Sort u_2} (f : ιβ) :
Subtype.val = f
theorem Set.surjective_onto_range {α : Type u_2} {ι : Sort u_1} {f : ια} :
theorem Set.image_eq_range {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
f '' s = Set.range fun x => f x
theorem Sum.range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α βγ) :
= Set.range (f Sum.inl) Set.range (f Sum.inr)
@[simp]
theorem Set.Sum.elim_range {α : Type u_3} {β : Type u_2} {γ : Type u_1} (f : αγ) (g : βγ) :
theorem Set.range_ite_subset' {α : Type u_2} {β : Type u_1} {p : Prop} [inst : ] {f : αβ} {g : αβ} :
Set.range (if p then f else g)
theorem Set.range_ite_subset {α : Type u_1} {β : Type u_2} {p : αProp} [inst : ] {f : αβ} {g : αβ} :
(Set.range fun x => if p x then f x else g x)
@[simp]
theorem Set.preimage_range {α : Type u_1} {β : Type u_2} (f : αβ) :
f ⁻¹' = Set.univ
theorem Set.range_unique {α : Type u_2} {ι : Sort u_1} {f : ια} [h : ] :
= {f default}

The range of a function from a unique type contains just the function applied to its single value.

theorem Set.range_diff_image_subset {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
\ f '' s f '' s
theorem Set.range_diff_image {α : Type u_1} {β : Type u_2} {f : αβ} (H : ) (s : Set α) :
\ f '' s = f '' s
@[simp]
theorem Set.range_inclusion {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
= { x | x s }
noncomputable def Set.rangeSplitting {α : Type u_1} {β : Type u_2} (f : αβ) :
↑()α

We can use the axiom of choice to pick a preimage for every element of range f.

Equations
theorem Set.apply_rangeSplitting {α : Type u_2} {β : Type u_1} (f : αβ) (x : ↑()) :
f () = x
@[simp]
theorem Set.comp_rangeSplitting {α : Type u_2} {β : Type u_1} (f : αβ) :
= Subtype.val
theorem Set.leftInverse_rangeSplitting {α : Type u_2} {β : Type u_1} (f : αβ) :
theorem Set.rangeSplitting_injective {α : Type u_2} {β : Type u_1} (f : αβ) :
theorem Set.rightInverse_rangeSplitting {α : Type u_1} {β : Type u_2} {f : αβ} (h : ) :
theorem Set.preimage_rangeSplitting {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) :
@[simp]
theorem Set.compl_range_some (α : Type u_1) :
Set.range some = {none}
@[simp]
theorem Set.range_some_inter_none (α : Type u_1) :
Set.range some {none} =
theorem Set.range_some_union_none (α : Type u_1) :
Set.range some {none} = Set.univ
@[simp]
theorem Set.insert_none_range_some (α : Type u_1) :
insert none (Set.range some) = Set.univ
theorem Set.Subsingleton.image {α : Type u_1} {β : Type u_2} {s : Set α} (hs : ) (f : αβ) :

The image of a subsingleton is a subsingleton.

theorem Set.Subsingleton.preimage {α : Type u_2} {β : Type u_1} {s : Set β} (hs : ) {f : αβ} (hf : ) :

The preimage of a subsingleton under an injective map is a subsingleton.

theorem Set.subsingleton_of_image {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set α) (hs : Set.Subsingleton (f '' s)) :

If the image of a set under an injective map is a subsingleton, the set is a subsingleton.

theorem Set.subsingleton_of_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set β) (hs : Set.Subsingleton (f ⁻¹' s)) :

If the preimage of a set under an surjective map is a subsingleton, the set is a subsingleton.

theorem Set.subsingleton_range {β : Type u_2} {α : Sort u_1} [inst : ] (f : αβ) :
theorem Set.Nontrivial.preimage {α : Type u_2} {β : Type u_1} {s : Set β} (hs : ) {f : αβ} (hf : ) :

The preimage of a nontrivial set under a surjective map is nontrivial.

theorem Set.Nontrivial.image {α : Type u_1} {β : Type u_2} {s : Set α} (hs : ) {f : αβ} (hf : ) :

The image of a nontrivial set under an injective map is nontrivial.

theorem Set.nontrivial_of_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (hs : Set.Nontrivial (f '' s)) :

If the image of a set is nontrivial, the set is nontrivial.

theorem Set.nontrivial_of_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set β) (hs : Set.Nontrivial (f ⁻¹' s)) :

If the preimage of a set under an injective map is nontrivial, the set is nontrivial.

theorem Function.Surjective.preimage_injective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) :
theorem Function.Injective.preimage_image {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set α) :
f ⁻¹' (f '' s) = s
theorem Function.Injective.preimage_surjective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) :
theorem Function.Injective.subsingleton_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {s : Set α} :
theorem Function.Surjective.image_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set β) :
f '' (f ⁻¹' s) = s
theorem Function.Surjective.image_surjective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) :
theorem Function.Surjective.nonempty_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {s : Set β} :
theorem Function.Injective.image_injective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) :
theorem Function.Surjective.preimage_subset_preimage_iff {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} {t : Set β} (hf : ) :
f ⁻¹' s f ⁻¹' t s t
theorem Function.Surjective.range_comp {ι : Sort u_2} {α : Type u_3} {ι' : Sort u_1} {f : ιι'} (hf : ) (g : ι'α) :
Set.range (g f) =
theorem Function.Injective.mem_range_iff_exists_unique {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {b : β} :
b ∃! a, f a = b
theorem Function.Injective.exists_unique_of_mem_range {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {b : β} (hb : b ) :
∃! a, f a = b
theorem Function.Injective.compl_image_eq {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set α) :
(f '' s) = f '' s
theorem Function.LeftInverse.image_image {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : ) (s : Set α) :
g '' (f '' s) = s
theorem Function.LeftInverse.preimage_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h : ) (s : Set α) :
f ⁻¹' (g ⁻¹' s) = s
@[simp]
theorem EquivLike.range_comp {ι : Sort u_2} {ι' : Sort u_3} {E : Type u_4} [inst : EquivLike E ι ι'] {α : Type u_1} (f : ι'α) (e : E) :
Set.range (f e) =

### Image and preimage on subtypes #

theorem Subtype.coe_image {α : Type u_1} {p : αProp} {s : Set ()} :
Subtype.val '' s = { x | h, { val := x, property := h } s }
@[simp]
theorem Subtype.coe_image_of_subset {α : Type u_1} {s : Set α} {t : Set α} (h : t s) :
Subtype.val '' { x | x t } = t
theorem Subtype.range_coe {α : Type u_1} {s : Set α} :
Set.range Subtype.val = s
theorem Subtype.range_val {α : Type u_1} {s : Set α} :
Set.range Subtype.val = s

A variant of range_coe. Try to use range_coe if possible. This version is useful when defining a new type that is defined as the subtype of something. In that case, the coercion doesn't fire anymore.

@[simp]
theorem Subtype.range_coe_subtype {α : Type u_1} {p : αProp} :
Set.range Subtype.val = { x | p x }

We make this the simp lemma instead of range_coe. The reason is that if we write for s : Set α the function (↑) : s → α↑) : s → α→ α, then the inferred implicit arguments of (↑)↑) are ↑α (λ x, x ∈ s)↑α (λ x, x ∈ s)∈ s).

@[simp]
theorem Subtype.coe_preimage_self {α : Type u_1} (s : Set α) :
Subtype.val ⁻¹' s = Set.univ
theorem Subtype.range_val_subtype {α : Type u_1} {p : αProp} :
Set.range Subtype.val = { x | p x }
theorem Subtype.coe_image_subset {α : Type u_1} (s : Set α) (t : Set s) :
Subtype.val '' t s
theorem Subtype.coe_image_univ {α : Type u_1} (s : Set α) :
Subtype.val '' Set.univ = s
@[simp]
theorem Subtype.image_preimage_coe {α : Type u_1} (s : Set α) (t : Set α) :
Subtype.val '' (Subtype.val ⁻¹' t) = t s
theorem Subtype.image_preimage_val {α : Type u_1} (s : Set α) (t : Set α) :
Subtype.val '' (Subtype.val ⁻¹' t) = t s
theorem Subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} :
Subtype.val ⁻¹' t = Subtype.val ⁻¹' u t s = u s
theorem Subtype.preimage_coe_inter_self {α : Type u_1} (s : Set α) (t : Set α) :
Subtype.val ⁻¹' (t s) = Subtype.val ⁻¹' t
theorem Subtype.preimage_val_eq_preimage_val_iff {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) :
Subtype.val ⁻¹' t = Subtype.val ⁻¹' u t s = u s
theorem Subtype.exists_set_subtype {α : Type u_1} {t : Set α} (p : Set αProp) :
(s, p (Subtype.val '' s)) s, s t p s
theorem Subtype.forall_set_subtype {α : Type u_1} {t : Set α} (p : Set αProp) :
((s : Set t) → p (Subtype.val '' s)) (s : Set α) → s tp s
theorem Subtype.preimage_coe_nonempty {α : Type u_1} {s : Set α} {t : Set α} :
Set.Nonempty (Subtype.val ⁻¹' t) Set.Nonempty (s t)
theorem Subtype.preimage_coe_eq_empty {α : Type u_1} {s : Set α} {t : Set α} :
Subtype.val ⁻¹' t = s t =
theorem Subtype.preimage_coe_compl {α : Type u_1} (s : Set α) :
Subtype.val ⁻¹' s =
@[simp]
theorem Subtype.preimage_coe_compl' {α : Type u_1} (s : Set α) :
(fun x => x) ⁻¹' s =

### Images and preimages on Option#

theorem Option.injective_iff {α : Type u_1} {β : Type u_2} {f : β} :
Function.Injective (f some) ¬f none Set.range (f some)
theorem Option.range_eq {α : Type u_1} {β : Type u_2} (f : β) :
= insert (f none) (Set.range (f some))
theorem WithBot.range_eq {α : Type u_1} {β : Type u_2} (f : β) :
= insert (f ) (Set.range (f WithBot.some))
theorem WithTop.range_eq {α : Type u_1} {β : Type u_2} (f : β) :
= insert (f ) (Set.range (f WithBot.some))

### Injectivity and surjectivity lemmas for image and preimage #

@[simp]
theorem Set.preimage_injective {α : Type u} {β : Type v} {f : αβ} :
@[simp]
theorem Set.preimage_surjective {α : Type u} {β : Type v} {f : αβ} :
@[simp]
theorem Set.image_surjective {α : Type u} {β : Type v} {f : αβ} :
@[simp]
theorem Set.image_injective {α : Type u} {β : Type v} {f : αβ} :
theorem Set.preimage_eq_iff_eq_image {α : Type u} {β : Type v} {f : αβ} (hf : ) {s : Set β} {t : Set α} :
f ⁻¹' s = t s = f '' t
theorem Set.eq_preimage_iff_image_eq {α : Type u} {β : Type v} {f : αβ} (hf : ) {s : Set α} {t : Set β} :
s = f ⁻¹' t f '' s = t

### Disjoint lemmas for image and preimage #

theorem Disjoint.preimage {α : Type u_2} {β : Type u_1} (f : αβ) {s : Set β} {t : Set β} (h : Disjoint s t) :
Disjoint (f ⁻¹' s) (f ⁻¹' t)
theorem Set.disjoint_image_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : βα} {g : γα} {s : Set β} {t : Set γ} (h : ∀ (b : β), b s∀ (c : γ), c tf b g c) :
Disjoint (f '' s) (g '' t)
theorem Set.disjoint_image_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {s : Set α} {t : Set α} (hd : Disjoint s t) :
Disjoint (f '' s) (f '' t)
theorem Disjoint.of_image {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set α} {t : Set α} (h : Disjoint (f '' s) (f '' t)) :
theorem Set.disjoint_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} (hf : ) :
Disjoint (f '' s) (f '' t) Disjoint s t
theorem Disjoint.of_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {s : Set β} {t : Set β} (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) :
theorem Set.disjoint_preimage_iff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) {s : Set β} {t : Set β} :
theorem Set.preimage_eq_empty {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} (h : Disjoint s ()) :
theorem Set.preimage_eq_empty_iff {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set β} :