data.set.image

# Images and preimages of sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• preimage f t : set α : the preimage f⁻¹(t) (written f ⁻¹' 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)

## 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, is the set of x : α such that f x ∈ s.

Equations
Instances for set.preimage
Instances for set.preimage
@[simp]
theorem set.preimage_empty {α : Type u_1} {β : Type u_2} {f : α β} :
@[simp]
theorem set.mem_preimage {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} {a : α} :
a f ⁻¹' s f a s
theorem set.preimage_congr {α : Type u_1} {β : Type u_2} {f g : α β} {s : set β} (h : (x : α), f x = g x) :
f ⁻¹' s = g ⁻¹' s
theorem set.preimage_mono {α : Type u_1} {β : Type u_2} {f : α β} {s t : set β} (h : s t) :
f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_univ {α : Type u_1} {β : Type u_2} {f : α β} :
theorem set.subset_preimage_univ {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} :
s
@[simp]
theorem set.preimage_inter {α : Type u_1} {β : Type u_2} {f : α β} {s t : set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_union {α : Type u_1} {β : Type u_2} {f : α β} {s t : set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_compl {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
@[simp]
theorem set.preimage_diff {α : Type u_1} {β : Type u_2} (f : α β) (s t : set β) :
f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
@[simp]
theorem set.preimage_ite {α : Type u_1} {β : Type u_2} (f : α β) (s t₁ t₂ : set β) :
f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)
@[simp]
theorem set.preimage_set_of_eq {α : Type u_1} {β : Type u_2} {p : α Prop} {f : β α} :
f ⁻¹' {a : α | p a} = {a : β | p (f a)}
@[simp]
theorem set.preimage_id_eq {α : Type u_1} :
theorem set.preimage_id {α : Type u_1} {s : set α} :
= s
@[simp]
theorem set.preimage_id' {α : Type u_1} {s : set α} :
(λ (x : α), x) ⁻¹' s = s
@[simp]
theorem set.preimage_const_of_mem {α : Type u_1} {β : Type u_2} {b : β} {s : set β} (h : b s) :
(λ (x : α), b) ⁻¹' s = set.univ
@[simp]
theorem set.preimage_const_of_not_mem {α : Type u_1} {β : Type u_2} {b : β} {s : set β} (h : b s) :
(λ (x : α), b) ⁻¹' s =
theorem set.preimage_const {α : Type u_1} {β : Type u_2} (b : β) (s : set β) [decidable (b s)] :
(λ (x : α), b) ⁻¹' s = ite (b s) set.univ
theorem set.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} {s : set γ} :
g f ⁻¹' s = f ⁻¹' (g ⁻¹' s)
theorem set.preimage_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} :
@[simp]
theorem set.preimage_iterate_eq {α : Type u_1} {f : α α} {n : } :
= ^[n])
theorem set.preimage_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} {s : set γ} :
f ⁻¹' (g ⁻¹' s) = (λ (x : α), g (f x)) ⁻¹' s
theorem set.eq_preimage_subtype_val_iff {α : Type u_1} {p : α Prop} {s : set (subtype p)} {t : set α} :
s = (x : α) (h : p x), x, h⟩ s x t
theorem set.nonempty_of_nonempty_preimage {α : Type u_1} {β : Type u_2} {s : set β} {f : α β} (hf : (f ⁻¹' s).nonempty) :
theorem set.preimage_subtype_coe_eq_compl {α : Type u_1} {s u v : set α} (hsuv : s u v) (H : s (u v) = ) :

### Image of a set under a function #

def set.image {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
set β

The image of s : set α by f : α → β, written f '' s, is the set of y : β such that f x = y for some x ∈ s.

Equations
Instances for set.image
Instances for set.image
theorem set.mem_image_iff_bex {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {y : β} :
y f '' s (x : α) (_x : x s), 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_1} {β : Type u_2} {s : set α} (f : α β) :
f '' s = (λ (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 : function.injective f) {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 '' s p y) (x : α), x s p (f x)
theorem set.ball_image_of_ball {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {p : β Prop} (h : (x : α), x s p (f x)) (y : β) (H : y f '' s) :
p y
theorem set.bex_image_iff {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {p : β Prop} :
( (y : β) (H : y f '' s), p y) (x : α) (H : x s), p (f x)
theorem set.mem_image_elim {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} {C : β Prop} (h : (x : α), x s C (f x)) {y : β} :
y f '' s C 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 s C (f x)) :
C y
theorem set.image_congr {α : Type u_1} {β : Type u_2} {f g : α β} {s : set α} (h : (a : α), a s f 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_2} {γ : Type u_3} (f : β γ) (g : α β) (a : set α) :
f g '' a = f '' (g '' a)
theorem set.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : α β) (s : set α) :
g '' (f '' s) = (λ (x : α), g (f x)) '' s

A variant of image_comp, useful for rewriting

theorem set.image_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {β' : Type u_4} {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 : gb) :
(set.image ga) (set.image gb)
theorem function.commute.set_image {α : Type u_1} {f g : α α} (h : g) :
theorem set.image_subset {α : Type u_1} {β : Type u_2} {a 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 t : set α) :
f '' (s t) = f '' s f '' t
@[simp]
theorem set.image_empty {α : Type u_1} {β : Type u_2} (f : α β) :
theorem set.image_inter_subset {α : Type u_1} {β : Type u_2} (f : α β) (s t : set α) :
f '' (s t) f '' s f '' t
theorem set.image_inter_on {α : Type u_1} {β : Type u_2} {f : α β} {s t : set α} (h : (x : α), x t (y : α), y s f x = f y x = y) :
f '' (s t) = f '' s f '' t
theorem set.image_inter {α : Type u_1} {β : Type u_2} {f : α β} {s t : set α} (H : function.injective f) :
f '' (s t) = f '' s f '' t
theorem set.image_univ_of_surjective {β : Type u_2} {ι : Type u_1} {f : ι β} (H : function.surjective f) :
@[simp]
theorem set.image_singleton {α : Type u_1} {β : Type u_2} {f : α β} {a : α} :
f '' {a} = {f a}
@[simp]
theorem set.nonempty.image_const {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.nonempty) (a : β) :
(λ (_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} (S : set α) :
theorem set.mem_compl_image {α : Type u_1} (t : α) (S : set α) :
t S
@[simp]
theorem set.image_id' {α : Type u_1} (s : set α) :
(λ (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} (S : set α) :
theorem set.image_insert_eq {α : Type u_1} {β : Type u_2} {f : α β} {a : α} {s : set α} :
f '' = has_insert.insert (f a) (f '' s)
theorem set.image_pair {α : Type u_1} {β : Type u_2} (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 : f) (s : set α) :
f '' s g ⁻¹' s
theorem set.preimage_subset_image_of_inverse {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} (I : f) (s : set β) :
f ⁻¹' s g '' s
theorem set.image_eq_preimage_of_inverse {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} (h₁ : f) (h₂ : f) :
theorem set.mem_image_iff_of_inverse {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} {b : β} {s : set α} (h₁ : f) (h₂ : f) :
b f '' s g b s
theorem set.image_compl_subset {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} (H : function.injective f) :
f '' s (f '' s)
theorem set.subset_image_compl {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} (H : function.surjective f) :
(f '' s) f '' s
theorem set.image_compl_eq {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} (H : function.bijective f) :
f '' s = (f '' s)
theorem set.subset_image_diff {α : Type u_1} {β : Type u_2} (f : α β) (s t : set α) :
f '' s \ f '' t f '' (s \ t)
theorem set.subset_image_symm_diff {α : Type u_1} {β : Type u_2} {f : α β} {s t : set α} :
(f '' s) (f '' t) f '' s t
theorem set.image_diff {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (s t : set α) :
f '' (s \ t) = f '' s \ f '' t
theorem set.image_symm_diff {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (s t : set α) :
f '' s t = (f '' s) (f '' t)
theorem set.nonempty.image {α : Type u_1} {β : Type u_2} (f : α β) {s : set α} :
theorem set.nonempty.of_image {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} :
@[simp]
theorem set.nonempty_image_iff {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} :
theorem set.nonempty.preimage {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.nonempty) {f : α β} (hf : function.surjective f) :
@[protected, instance]
def set.image.nonempty {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) [nonempty s] :
@[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_1} {β : Type u_2} (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 : function.injective f) :
f ⁻¹' (f '' s) = s
theorem set.image_preimage_eq {α : Type u_1} {β : Type u_2} {f : α β} (s : set β) (h : function.surjective f) :
f '' (f ⁻¹' s) = s
theorem set.preimage_eq_preimage {α : Type u_1} {β : Type u_2} {s t : set α} {f : β α} (hf : function.surjective f) :
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 β} :
(f '' s t).nonempty (s f ⁻¹' t).nonempty
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} :
has_compl.compl '' {s : set α | p s} = {s : set α | 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 B a A
theorem set.image_eq_image {α : Type u_1} {β : Type u_2} {s t : set α} {f : α β} (hf : function.injective f) :
f '' s = f '' t s = t
theorem set.image_subset_image_iff {α : Type u_1} {β : Type u_2} {s t : set α} {f : α β} (hf : function.injective f) :
f '' s f '' t s t
theorem set.prod_quotient_preimage_eq_image {α : Type u_1} {β : Type u_2} [s : setoid α] (g : β) {h : α β} (Hh : h = ) (r : set × β)) :
{x : | (g x.fst, g x.snd) r} = (λ (a : α × α), (a.fst, a.snd)) '' ((λ (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 : (f '' x)), P a) (a : x), P (f a)
def set.image_factorization {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
s (f '' s)

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

Equations
theorem set.image_factorization_eq {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} :
theorem set.surjective_onto_image {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} :
theorem set.image_perm {α : Type u_1} {s : set α} {σ : equiv.perm α} (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 is 𝒫 s together with {a} ∪ t for each t ∈ 𝒫 s.

### Lemmas about range of a function. #

def set.range {α : Type u_1} {ι : Sort u_4} (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}
Instances for set.range
Instances for set.range
@[simp]
theorem set.mem_range {α : Type u_1} {ι : Sort u_4} {f : ι α} {x : α} :
x (y : ι), f y = x
@[simp]
theorem set.mem_range_self {α : Type u_1} {ι : Sort u_4} {f : ι α} (i : ι) :
f i
theorem set.forall_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι α} {p : α Prop} :
( (a : α), a p a) (i : ι), p (f i)
theorem set.forall_subtype_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι α} {p : (set.range f) Prop} :
( (a : (set.range f)), p a) (i : ι), p f i, _⟩
theorem set.exists_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι α} {p : α Prop} :
( (a : α) (H : a , p a) (i : ι), p (f i)
theorem set.exists_range_iff' {α : Type u_1} {ι : Sort u_4} {f : ι α} {p : α Prop} :
( (a : α), a p a) (i : ι), p (f i)
theorem set.exists_subtype_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι α} {p : (set.range f) Prop} :
( (a : (set.range f)), p a) (i : ι), p f i, _⟩
theorem set.range_iff_surjective {α : Type u_1} {ι : Sort u_4} {f : ι α} :
theorem function.surjective.range_eq {α : Type u_1} {ι : Sort u_4} {f : ι α} :

Alias of the reverse direction of set.range_iff_surjective.

@[simp]
theorem set.image_univ {α : Type u_1} {β : Type u_2} {f : α β} :
=
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_1} {β : Type u_2} {s : set β} (hs : s.nonempty) {f : α β} (hf : s ) :
theorem set.range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α β) (f : ι α) :
set.range (g f) = g ''
theorem set.range_subset_iff {α : Type u_1} {ι : Sort u_4} {f : ι α} {s : set α} :
s (y : ι), f y s
theorem set.range_eq_iff {α : Type u_1} {β : Type u_2} (f : α β) (s : set β) :
= s ( (a : α), f a s) (b : β), b s ( (a : α), f a = b)
theorem set.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) :
theorem set.range_nonempty_iff_nonempty {α : Type u_1} {ι : Sort u_4} {f : ι α} :
theorem set.range_nonempty {α : Type u_1} {ι : Sort u_4} [h : nonempty ι] (f : ι α) :
@[simp]
theorem set.range_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ι α} :
theorem set.range_eq_empty {α : Type u_1} {ι : Sort u_4} [is_empty ι] (f : ι α) :
@[protected, instance]
def set.range.nonempty {α : Type u_1} {ι : Sort u_4} [nonempty ι] (f : ι α) :
@[simp]
theorem set.image_union_image_compl_eq_range {α : Type u_1} {β : Type u_2} {s : set α} (f : α β) :
f '' s f '' s =
theorem set.insert_image_compl_eq_range {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
has_insert.insert (f x) (f '' {x}) =
theorem set.image_preimage_eq_inter_range {α : Type u_1} {β : Type u_2} {f : α β} {t : set β} :
f '' (f ⁻¹' t) = t
theorem set.image_preimage_eq_of_subset {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} (hs : s ) :
f '' (f ⁻¹' s) = s
theorem set.image_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
f '' (f ⁻¹' s) = s s
theorem set.subset_range_iff_exists_image_eq {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
s (t : set α), f '' t = s
@[simp]
theorem set.exists_subset_range_and_iff {α : Type u_1} {β : Type u_2} {f : α β} {p : set β Prop} :
( (s : set β), s p s) (s : set α), p (f '' s)
theorem set.exists_subset_range_iff {α : Type u_1} {β : Type u_2} {f : α β} {p : set β Prop} :
( (s : set β) (H : s , p s) (s : set α), p (f '' s)
theorem set.range_image {α : Type u_1} {β : Type u_2} (f : α β) :
theorem set.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {s t : set α} {f : β α} (hs : s ) :
f ⁻¹' s f ⁻¹' t s t
theorem set.preimage_eq_preimage' {α : Type u_1} {β : Type u_2} {s t : set α} {f : β α} (hs : s ) (ht : t ) :
f ⁻¹' s = f ⁻¹' t s = t
@[simp]
theorem set.preimage_inter_range {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
f ⁻¹' (s = f ⁻¹' s
@[simp]
theorem set.preimage_range_inter {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
f ⁻¹' s) = f ⁻¹' s
theorem set.preimage_image_preimage {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
@[simp]
theorem set.range_id {α : Type u_1} :
@[simp]
theorem set.range_id' {α : Type u_1} :
set.range (λ (x : α), x) = set.univ
@[simp]
theorem prod.range_fst {α : Type u_1} {β : Type u_2} [nonempty β] :
@[simp]
theorem prod.range_snd {α : Type u_1} {β : Type u_2} [nonempty α] :
@[simp]
theorem set.range_eval {ι : Type u_1} {α : ι Type u_2} [ (i : ι), nonempty (α i)] (i : ι) :
theorem set.range_inl {α : Type u_1} {β : Type u_2} :
= {x : α β | (x.is_left)}
theorem set.range_inr {α : Type u_1} {β : Type u_2} :
= {x : α β | (x.is_right)}
theorem set.is_compl_range_inl_range_inr {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.range_inl_union_range_inr {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.range_inl_inter_range_inr {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.range_inr_union_range_inl {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.range_inr_inter_range_inl {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.preimage_inl_image_inr {α : Type u_1} {β : Type u_2} (s : set β) :
@[simp]
theorem set.preimage_inr_image_inl {α : Type u_1} {β : Type u_2} (s : set α) :
@[simp]
theorem set.preimage_inl_range_inr {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.preimage_inr_range_inl {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.compl_range_inl {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.compl_range_inr {α : Type u_1} {β : Type u_2} :
@[simp]
theorem set.range_quot_mk {α : Type u_1} (r : α α Prop) :
set.range (quot.mk r) = set.univ
@[simp]
theorem set.range_quot_lift {α : Type u_1} {ι : Sort u_4} {f : ι α} {r : ι ι Prop} (hf : (x y : ι), r x y f x = f y) :
set.range (quot.lift f hf) =
@[simp]
theorem set.range_quotient_mk {α : Type u_1} [setoid α] :
set.range (λ (x : α), x) = set.univ
@[simp]
theorem set.range_quotient_lift {α : Type u_1} {ι : Sort u_4} {f : ι α} [s : setoid ι] (hf : (a b : ι), a b f a = f b) :
@[simp]
theorem set.range_quotient_mk' {α : Type u_1} {s : setoid α} :
@[simp]
theorem set.range_quotient_lift_on' {α : Type u_1} {ι : Sort u_4} {f : ι α} {s : setoid ι} (hf : (a b : ι), b f a = f b) :
set.range (λ (x : quotient s), x.lift_on' f hf) =
@[protected, instance]
def set.can_lift {α : Type u_1} {β : Type u_2} (c : out_param α)) (p : out_param Prop)) [ β c p] :
can_lift (set α) (set β) (set.image c) (λ (s : set α), (x : α), x s p x)
Equations
theorem set.range_const_subset {α : Type u_1} {ι : Sort u_4} {c : α} :
set.range (λ (x : ι), c) {c}
@[simp]
theorem set.range_const {α : Type u_1} {ι : Sort u_4} [nonempty ι] {c : α} :
set.range (λ (x : ι), c) = {c}
theorem set.range_subtype_map {α : Type u_1} {β : Type u_2} {p : α Prop} {q : β Prop} (f : α β) (h : (x : α), p x q (f x)) :
set.range h) = coe ⁻¹' (f '' {x : α | p x})
theorem set.image_swap_eq_preimage_swap {α : Type u_1} {β : Type u_2} :
theorem set.preimage_singleton_nonempty {α : Type u_1} {β : Type u_2} {f : α β} {y : β} :
(f ⁻¹' {y}).nonempty 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_4} {f : ι α} {x : α} :
{x} f =
theorem set.image_compl_preimage {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :
f '' (f ⁻¹' s) = \ s
def set.range_factorization {β : Type u_2} {ι : Sort u_4} (f : ι β) :

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

Equations
• = λ (i : ι), f i, _⟩
theorem set.range_factorization_eq {β : Type u_2} {ι : Sort u_4} {f : ι β} :
@[simp]
theorem set.range_factorization_coe {β : Type u_2} {ι : Sort u_4} (f : ι β) (a : ι) :
= f a
@[simp]
theorem set.coe_comp_range_factorization {β : Type u_2} {ι : Sort u_4} (f : ι β) :
theorem set.surjective_onto_range {α : Type u_1} {ι : Sort u_4} {f : ι α} :
theorem set.image_eq_range {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
f '' s = set.range (λ (x : s), f x)
theorem sum.range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) :
@[simp]
theorem set.sum.elim_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) (g : β γ) :
theorem set.range_ite_subset' {α : Type u_1} {β : Type u_2} {p : Prop} [decidable p] {f g : α β} :
set.range (ite p f g)
theorem set.range_ite_subset {α : Type u_1} {β : Type u_2} {p : α Prop} {f g : α β} :
set.range (λ (x : α), ite (p x) (f x) (g x))
@[simp]
theorem set.preimage_range {α : Type u_1} {β : Type u_2} (f : α β) :
theorem set.range_unique {α : Type u_1} {ι : Sort u_4} {f : ι α} [h : unique ι] :

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 : function.injective f) (s : set α) :
\ f '' s = f '' s
@[simp]
theorem set.range_inclusion {α : Type u_1} {s t : set α} (h : s t) :
= {x : t | x s}
@[irreducible]
noncomputable def set.range_splitting {α : 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_range_splitting {α : Type u_1} {β : Type u_2} (f : α β) (x : (set.range f)) :
f x) = x
@[simp]
theorem set.comp_range_splitting {α : Type u_1} {β : Type u_2} (f : α β) :
theorem set.left_inverse_range_splitting {α : Type u_1} {β : Type u_2} (f : α β) :
theorem set.range_splitting_injective {α : Type u_1} {β : Type u_2} (f : α β) :
theorem set.right_inverse_range_splitting {α : Type u_1} {β : Type u_2} {f : α β} (h : function.injective f) :
theorem set.preimage_range_splitting {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) :
theorem set.is_compl_range_some_none (α : Type u_1) :
@[simp]
theorem set.compl_range_some (α : Type u_1) :
@[simp]
theorem set.range_some_inter_none (α : Type u_1) :
@[simp]
theorem set.range_some_union_none (α : Type u_1) :
@[simp]
theorem set.insert_none_range_some (α : Type u_1) :
theorem set.subsingleton.image {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.subsingleton) (f : α β) :

The image of a subsingleton is a subsingleton.

theorem set.subsingleton.preimage {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.subsingleton) {f : α β} (hf : function.injective f) :

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 : function.injective f) (s : set α) (hs : (f '' s).subsingleton) :

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 : function.surjective f) (s : set β) (hs : (f ⁻¹' s).subsingleton) :

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} [subsingleton α] (f : α β) :
theorem set.nontrivial.preimage {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.nontrivial) {f : α β} (hf : function.surjective f) :

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 : s.nontrivial) {f : α β} (hf : function.injective f) :

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 : (f '' s).nontrivial) :

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 : function.injective f) (s : set β) (hs : (f ⁻¹' s).nontrivial) :

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 : function.surjective f) :
theorem function.injective.preimage_image {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (s : set α) :
f ⁻¹' (f '' s) = s
theorem function.injective.preimage_surjective {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) :
theorem function.injective.subsingleton_image_iff {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) {s : set α} :
theorem function.surjective.image_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.surjective f) (s : set β) :
f '' (f ⁻¹' s) = s
theorem function.surjective.image_surjective {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.surjective f) :
theorem function.surjective.nonempty_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.surjective f) {s : set β} :
theorem function.injective.image_injective {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) :
theorem function.surjective.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {f : α β} {s t : set β} (hf : function.surjective f) :
f ⁻¹' s f ⁻¹' t s t
theorem function.surjective.range_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {f : ι ι'} (hf : function.surjective f) (g : ι' α) :
set.range (g f) =
theorem function.injective.mem_range_iff_exists_unique {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) {b : β} :
b ∃! (a : α), f a = b
theorem function.injective.exists_unique_of_mem_range {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) {b : β} (hb : b ) :
∃! (a : α), f a = b
theorem function.injective.compl_image_eq {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (s : set α) :
(f '' s) = f '' s (set.range f)
theorem function.left_inverse.image_image {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} (h : f) (s : set α) :
g '' (f '' s) = s
theorem function.left_inverse.preimage_preimage {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} (h : f) (s : set α) :
f ⁻¹' (g ⁻¹' s) = s
@[simp]
theorem equiv_like.range_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {E : Type u_6} [ ι ι'] (f : ι' α) (e : E) :

### Image and preimage on subtypes #

theorem subtype.coe_image {α : Type u_1} {p : α Prop} {s : set (subtype p)} :
= {x : α | (h : p x), x, h⟩ s}
@[simp]
theorem subtype.coe_image_of_subset {α : Type u_1} {s t : set α} (h : t s) :
coe '' {x : s | x t} = t
theorem subtype.range_coe {α : Type u_1} {s : set α} :
theorem subtype.range_val {α : Type u_1} {s : set α} :

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} :
= {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 coe : s → α, then the inferred implicit arguments of coe are coe α (λ x, x ∈ s).

@[simp]
theorem subtype.coe_preimage_self {α : Type u_1} (s : set α) :
theorem subtype.range_val_subtype {α : Type u_1} {p : α Prop} :
= {x : α | p x}
theorem subtype.coe_image_subset {α : Type u_1} (s : set α) (t : set s) :
s
theorem subtype.coe_image_univ {α : Type u_1} (s : set α) :
@[simp]
theorem subtype.image_preimage_coe {α : Type u_1} (s t : set α) :
coe '' (coe ⁻¹' t) = t s
theorem subtype.image_preimage_val {α : Type u_1} (s t : set α) :
= t s
theorem subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s t u : set α} :
= t s = u s
@[simp]
theorem subtype.preimage_coe_inter_self {α : Type u_1} (s t : set α) :
coe ⁻¹' (t s) =
theorem subtype.preimage_val_eq_preimage_val_iff {α : Type u_1} (s t u : set α) :
t s = u s
theorem subtype.exists_set_subtype {α : Type u_1} {t : set α} (p : set α Prop) :
( (s : set t), p (coe '' s)) (s : set α), s t p s
theorem subtype.preimage_coe_nonempty {α : Type u_1} {s t : set α} :
theorem subtype.preimage_coe_eq_empty {α : Type u_1} {s t : set α} :
= s t =
@[simp]
theorem subtype.preimage_coe_compl {α : Type u_1} (s : set α) :
@[simp]
theorem subtype.preimage_coe_compl' {α : Type u_1} (s : set α) :

### Images and preimages on option#

theorem option.injective_iff {α : Type u_1} {β : Type u_2} {f : β} :
theorem option.range_eq {α : Type u_1} {β : Type u_2} (f : β) :
theorem with_bot.range_eq {α : Type u_1} {β : Type u_2} (f : β) :
theorem with_top.range_eq {α : Type u_1} {β : Type u_2} (f : β) :

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

@[simp]
theorem set.preimage_injective {α : Type u_1} {β : Type u_2} {f : α β} :
@[simp]
theorem set.preimage_surjective {α : Type u_1} {β : Type u_2} {f : α β} :
@[simp]
theorem set.image_surjective {α : Type u_1} {β : Type u_2} {f : α β} :
@[simp]
theorem set.image_injective {α : Type u_1} {β : Type u_2} {f : α β} :
theorem set.preimage_eq_iff_eq_image {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.bijective f) {s : set β} {t : set α} :
f ⁻¹' s = t s = f '' t
theorem set.eq_preimage_iff_image_eq {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.bijective f) {s : set α} {t : set β} :
s = f ⁻¹' t f '' s = t

### Disjoint lemmas for image and preimage #

theorem disjoint.preimage {α : Type u_1} {β : Type u_2} (f : α β) {s t : set β} (h : t) :
disjoint (f ⁻¹' s) (f ⁻¹' t)
theorem set.disjoint_image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β α} {g : γ α} {s : set β} {t : set γ} (h : (b : β), b s (c : γ), c t f b g c) :
disjoint (f '' s) (g '' t)
theorem set.disjoint_image_of_injective {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) {s t : set α} (hd : t) :
disjoint (f '' s) (f '' t)
theorem disjoint.of_image {α : Type u_1} {β : Type u_2} {f : α β} {s t : set α} (h : disjoint (f '' s) (f '' t)) :
t
theorem set.disjoint_image_iff {α : Type u_1} {β : Type u_2} {f : α β} {s t : set α} (hf : function.injective f) :
disjoint (f '' s) (f '' t) t
theorem disjoint.of_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.surjective f) {s t : set β} (h : disjoint (f ⁻¹' s) (f ⁻¹' t)) :
t
theorem set.disjoint_preimage_iff {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.surjective f) {s t : set β} :
disjoint (f ⁻¹' s) (f ⁻¹' t) t
theorem set.preimage_eq_empty {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} (h : (set.range f)) :
theorem set.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} {f : α β} {s : set β} :