Documentation

Mathlib.Data.Set.Image

Images and preimages of sets #

Main definitions #

Notation #

Tags #

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

Inverse image #

@[simp]
theorem Set.preimage_empty {α : Type u_1} {β : Type u_2} {f : αβ} :
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 : 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_1} {β : Type u_2} {f : αβ} {s : Set β} {t : Set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem Set.preimage_union {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} {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 : Set β) (t : Set β) :
f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
@[simp]
theorem Set.preimage_symmDiff {α : Type u_1} {β : Type u_2} {f : αβ} (s : Set β) (t : Set β) :
@[simp]
theorem Set.preimage_ite {α : Type u_1} {β : Type u_2} (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_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 α} :
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_1} {β : Type u_2} {b : β} {s : Set β} (h : b s) :
(fun (x : α) => b) ⁻¹' s = Set.univ
@[simp]
theorem Set.preimage_const_of_not_mem {α : Type u_1} {β : Type u_2} {b : β} {s : Set β} (h : bs) :
(fun (x : α) => b) ⁻¹' s =
theorem Set.preimage_const {α : Type u_1} {β : Type u_2} (b : β) (s : Set β) [Decidable (b s)] :
(fun (x : α) => b) ⁻¹' s = if b s then Set.univ else
theorem Set.exists_eq_const_of_preimage_singleton {α : Type u_1} {β : Type u_2} [Nonempty β] {f : αβ} (hf : ∀ (b : β), f ⁻¹' {b} = f ⁻¹' {b} = Set.univ) :
∃ (b : β), f = Function.const α b

If preimage of each singleton under f : α → β is either empty or the whole type, then f is a constant.

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 : βγ} :
theorem Set.preimage_iterate_eq {α : Type u_1} {f : αα} {n : } :
theorem Set.preimage_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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 (Subtype p)} {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_1} {β : Type u_2} {s : Set β} {f : αβ} (hf : Set.Nonempty (f ⁻¹' s)) :
@[simp]
theorem Set.preimage_singleton_true {α : Type u_1} (p : αProp) :
p ⁻¹' {True} = {a : α | p a}
@[simp]
theorem Set.preimage_singleton_false {α : Type u_1} (p : αProp) :
p ⁻¹' {False} = {a : α | ¬p a}
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 #

theorem Set.mem_image_iff_bex {α : 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 = (fun (x : α) => f x) '' s
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} :
(yf '' s, p y) xs, p (f x)
theorem Set.ball_image_of_ball {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {p : βProp} (h : xs, p (f x)) (y : β) :
y f '' sp y
theorem Set.bex_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {p : βProp} :
(∃ y ∈ f '' s, p y) ∃ x ∈ s, p (f x)
theorem Set.mem_image_elim {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {C : βProp} (h : xs, C (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 : xs, C (f x)) :
C y
theorem Set.image_congr {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {s : Set α} (h : as, 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_mono {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} (h : s t) :
f '' s f '' t
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_comp_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : βγ} :
theorem Set.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {β' : Type u_6} {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 : Function.Commute f g) :
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_1} {β : Type u_2} (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 : xt, ys, f 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 : Function.Injective f) :
f '' (s t) = f '' s f '' t
theorem Set.image_univ_of_surjective {β : Type u_2} {ι : Type u_6} {f : ιβ} (H : Function.Surjective f) :
f '' Set.univ = Set.univ
@[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 : Set.Nonempty s) (a : β) :
(fun (x : α) => a) '' s = {a}
@[simp]
theorem Set.image_eq_empty {α : Type u_6} {β : Type u_7} {f : αβ} {s : Set α} :
f '' s = s =
theorem Set.preimage_compl_eq_image_compl {α : Type u_1} [BooleanAlgebra α] (S : Set α) :
compl ⁻¹' S = compl '' S
theorem Set.mem_compl_image {α : Type u_1} [BooleanAlgebra α] (t : α) (S : Set α) :
t compl '' S t S
@[simp]
theorem Set.image_id_eq {α : Type u_1} :
Set.image id = id
@[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.image_iterate_eq {α : Type u_1} {f : αα} {n : } :
theorem Set.compl_compl_image {α : Type u_1} [BooleanAlgebra α] (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_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 : Function.LeftInverse g f) (s : Set α) :
f '' s g ⁻¹' s
theorem Set.preimage_subset_image_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (I : Function.LeftInverse g f) (s : Set β) :
f ⁻¹' s g '' s
theorem Set.image_eq_preimage_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
theorem Set.mem_image_iff_of_inverse {α : Type u_1} {β : Type u_2} {f : αβ} {g : βα} {b : β} {s : Set α} (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g 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 : Set α) (t : Set α) :
f '' s \ f '' t f '' (s \ t)
theorem Set.subset_image_symmDiff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} :
symmDiff (f '' s) (f '' t) f '' symmDiff s t
theorem Set.image_diff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (s : Set α) (t : Set α) :
f '' (s \ t) = f '' s \ f '' t
theorem Set.image_symmDiff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (s : Set α) (t : Set α) :
f '' symmDiff s t = symmDiff (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.image_nonempty {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
@[deprecated Set.image_nonempty]
theorem Set.nonempty_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :

Alias of Set.image_nonempty.

theorem Set.Nonempty.preimage {α : Type u_1} {β : Type u_2} {s : Set β} (hs : Set.Nonempty s) {f : αβ} (hf : Function.Surjective f) :
instance Set.instNonemptyElemImage {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) [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_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)
@[simp]
theorem Set.preimage_image_eq {α : Type u_1} {β : Type u_2} {f : αβ} (s : Set α) (h : Function.Injective f) :
f ⁻¹' (f '' s) = s
@[simp]
theorem Set.image_preimage_eq {α : Type u_1} {β : Type u_2} {f : αβ} (s : Set β) (h : Function.Surjective f) :
f '' (f ⁻¹' s) = s
@[simp]
theorem Set.Nonempty.subset_preimage_const {α : Type u_1} {β : Type u_2} {s : Set α} (hs : Set.Nonempty s) (t : Set β) (a : β) :
s (fun (x : α) => a) ⁻¹' t a t
@[simp]
theorem Set.preimage_eq_preimage {α : Type u_1} {β : Type u_2} {s : Set α} {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 β} :
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 : 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 Ba A
theorem Set.image_eq_image {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : αβ} (hf : Function.Injective f) :
f '' s = f '' t s = t
theorem Set.subset_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set β} :
t f '' s ∃ u ⊆ s, f '' u = t
theorem Set.image_subset_image_iff {α : Type u_1} {β : Type u_2} {s : Set α} {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 : Quotient sβ) {h : αβ} (Hh : h = g Quotient.mk'') (r : Set (β × β)) :
{x : Quotient s × Quotient s | (g x.1, g x.2) r} = (fun (a : α × α) => (a.1, a.2)) '' ((fun (a : α × α) => (h a.1, h a.2)) ⁻¹' 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)
theorem Set.imageFactorization_eq {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
Subtype.val Set.imageFactorization f s = 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 α} {σ : 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. #

theorem Set.forall_range_iff {α : Type u_1} {ι : Sort u_4} {f : ια} {p : αProp} :
(aSet.range f, 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 { val := f i, property := (_ : f i Set.range f) }
theorem Set.exists_range_iff {α : Type u_1} {ι : Sort u_4} {f : ια} {p : α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 ∈ Set.range f, 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 { val := f i, property := (_ : f i Set.range f) }
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.subset_range_of_surjective {α : Type u_1} {β : Type u_2} {f : αβ} (h : Function.Surjective f) (s : Set β) :
@[simp]
theorem Set.image_univ {α : Type u_1} {β : Type u_2} {f : αβ} :
f '' Set.univ = Set.range f
@[simp]
theorem Set.preimage_eq_univ_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
f ⁻¹' s = Set.univ Set.range f s
theorem Set.image_subset_range {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
theorem Set.mem_range_of_mem_image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) {x : β} (h : x f '' s) :
theorem Set.Nonempty.preimage' {α : Type u_1} {β : Type u_2} {s : Set β} (hs : Set.Nonempty s) {f : αβ} (hf : s Set.range f) :
theorem Set.range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : αβ) (f : ια) :
theorem Set.range_subset_iff {α : Type u_1} {ι : Sort u_4} {f : ια} {s : Set α} :
Set.range f s ∀ (y : ι), f y s
theorem Set.range_subset_range_iff_exists_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} :
Set.range f Set.range g ∃ (h : αβ), f = g h
theorem Set.range_eq_iff {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
Set.range f = s (∀ (a : α), f a s) bs, ∃ (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} [IsEmpty ι] (f : ια) :
instance Set.instNonemptyRange {α : Type u_1} {ι : Sort u_4} [Nonempty ι] (f : ια) :
Equations
@[simp]
theorem Set.image_union_image_compl_eq_range {α : Type u_1} {β : Type u_2} {s : Set α} (f : αβ) :
f '' s f '' s = Set.range f
theorem Set.insert_image_compl_eq_range {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
insert (f x) (f '' {x}) = Set.range f
theorem Set.image_preimage_eq_range_inter {α : Type u_1} {β : Type u_2} {f : αβ} {t : Set β} :
f '' (f ⁻¹' t) = Set.range f t
theorem Set.image_preimage_eq_inter_range {α : Type u_1} {β : Type u_2} {f : αβ} {t : Set β} :
f '' (f ⁻¹' t) = t Set.range f
theorem Set.image_preimage_eq_of_subset {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} (hs : s Set.range f) :
f '' (f ⁻¹' s) = s
theorem Set.image_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
f '' (f ⁻¹' s) = s s Set.range f
theorem Set.subset_range_iff_exists_image_eq {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
s Set.range f ∃ (t : Set α), f '' t = s
theorem Set.range_image {α : Type u_1} {β : Type u_2} (f : αβ) :
@[simp]
theorem Set.exists_subset_range_and_iff {α : Type u_1} {β : Type u_2} {f : αβ} {p : Set βProp} :
(∃ s ⊆ Set.range f, 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 β) (_ : s Set.range f), p s) ∃ (s : Set α), p (f '' s)
theorem Set.forall_subset_range_iff {α : Type u_1} {β : Type u_2} {f : αβ} {p : Set βProp} :
(sSet.range f, p s) ∀ (s : Set α), p (f '' s)
@[simp]
theorem Set.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : βα} (hs : s Set.range f) :
f ⁻¹' s f ⁻¹' t s t
theorem Set.preimage_eq_preimage' {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set α} {f : βα} (hs : s Set.range f) (ht : t Set.range f) :
f ⁻¹' s = f ⁻¹' t s = t
theorem Set.preimage_inter_range {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
theorem Set.preimage_range_inter {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
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} :
Set.range id = Set.univ
@[simp]
theorem Set.range_id' {α : Type u_1} :
(Set.range fun (x : α) => x) = Set.univ
@[simp]
theorem Prod.range_fst {α : Type u_1} {β : Type u_2} [Nonempty β] :
Set.range Prod.fst = Set.univ
@[simp]
theorem Prod.range_snd {α : Type u_1} {β : Type u_2} [Nonempty α] :
Set.range Prod.snd = Set.univ
@[simp]
theorem Set.range_eval {ι : Sort u_4} {α : ιType u_6} [∀ (i : ι), Nonempty (α i)] (i : ι) :
theorem Set.range_inl {α : Type u_1} {β : Type u_2} :
Set.range Sum.inl = {x : α β | Sum.isLeft x = true}
theorem Set.range_inr {α : Type u_1} {β : Type u_2} :
Set.range Sum.inr = {x : α β | Sum.isRight x = true}
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_1} {β : Type u_2} (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_1} {β : Type u_2} :
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_1} {β : Type u_2} (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 (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 yf x = f y) :
@[simp]
theorem Set.range_quotient_mk {α : Type u_1} [sa : Setoid α] :
(Set.range fun (x : α) => x) = Set.univ
@[simp]
theorem Set.range_quotient_lift {α : Type u_1} {ι : Sort u_4} {f : ια} [s : Setoid ι] (hf : ∀ (a b : ι), a bf a = f b) :
@[simp]
theorem Set.range_quotient_mk' {α : Type u_1} {s : Setoid α} :
Set.range Quotient.mk' = Set.univ
@[simp]
theorem Set.Quotient.range_mk'' {α : Type u_1} {sa : Setoid α} :
Set.range Quotient.mk'' = Set.univ
@[simp]
theorem Set.range_quotient_lift_on' {α : Type u_1} {ι : Sort u_4} {f : ια} {s : Setoid ι} (hf : ∀ (a b : ι), Setoid.r a bf a = f b) :
(Set.range fun (x : Quotient s) => Quotient.liftOn' x f hf) = Set.range f
instance Set.canLift {α : Type u_1} {β : Type u_2} (c : βα) (p : αProp) [CanLift α β c p] :
CanLift (Set α) (Set β) (fun (x : Set β) => c '' x) fun (s : Set α) => xs, p x
Equations
theorem Set.range_const_subset {α : Type u_1} {ι : Sort u_4} {c : α} :
(Set.range fun (x : ι) => c) {c}
@[simp]
theorem Set.range_const {α : Type u_1} {ι : Sort u_4} [Nonempty ι] {c : α} :
(Set.range fun (x : ι) => c) = {c}
theorem Set.range_subtype_map {α : Type u_1} {β : Type u_2} {p : αProp} {q : βProp} (f : αβ) (h : ∀ (x : α), p xq (f x)) :
Set.range (Subtype.map f h) = 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} = ySet.range f
theorem Set.range_subset_singleton {α : Type u_1} {ι : Sort u_4} {f : ια} {x : α} :
theorem Set.image_compl_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
f '' (f ⁻¹' s) = Set.range f \ s
theorem Set.rangeFactorization_eq {β : Type u_2} {ι : Sort u_4} {f : ιβ} :
Subtype.val Set.rangeFactorization f = f
@[simp]
theorem Set.rangeFactorization_coe {β : Type u_2} {ι : Sort u_4} (f : ιβ) (a : ι) :
@[simp]
theorem Set.coe_comp_rangeFactorization {β : Type u_2} {ι : Sort u_4} (f : ιβ) :
Subtype.val Set.rangeFactorization f = 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 fun (x : s) => f x
theorem Sum.range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α βγ) :
Set.range f = Set.range (f Sum.inl) Set.range (f Sum.inr)
@[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 (if p then f else g) Set.range f Set.range g
theorem Set.range_ite_subset {α : Type u_1} {β : Type u_2} {p : αProp} [DecidablePred p] {f : αβ} {g : αβ} :
(Set.range fun (x : α) => if p x then f x else g x) Set.range f Set.range g
@[simp]
theorem Set.preimage_range {α : Type u_1} {β : Type u_2} (f : αβ) :
f ⁻¹' Set.range f = Set.univ
theorem Set.range_unique {α : Type u_1} {ι : Sort u_4} {f : ια} [h : Unique ι] :
Set.range f = {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 α) :
Set.range f \ f '' s f '' s
theorem Set.range_diff_image {α : Type u_1} {β : Type u_2} {f : αβ} (H : Function.Injective f) (s : Set α) :
Set.range f \ f '' s = f '' s
@[simp]
theorem Set.range_inclusion {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
Set.range (Set.inclusion h) = {x : t | x s}
theorem Set.rangeSplitting_injective {α : Type u_1} {β : Type u_2} (f : αβ) :
theorem Set.isCompl_range_some_none (α : Type u_6) :
IsCompl (Set.range some) {none}
@[simp]
theorem Set.compl_range_some (α : Type u_6) :
(Set.range some) = {none}
@[simp]
theorem Set.range_some_inter_none (α : Type u_6) :
Set.range some {none} =
theorem Set.range_some_union_none (α : Type u_6) :
Set.range some {none} = Set.univ
@[simp]
theorem Set.insert_none_range_some (α : Type u_6) :
insert none (Set.range some) = Set.univ
theorem Set.Subsingleton.image {α : Type u_1} {β : Type u_2} {s : Set α} (hs : Set.Subsingleton s) (f : αβ) :

The image of a subsingleton is a subsingleton.

theorem Set.Subsingleton.preimage {α : Type u_1} {β : Type u_2} {s : Set β} (hs : Set.Subsingleton s) {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 : 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 : Function.Surjective f) (s : Set β) (hs : Set.Subsingleton (f ⁻¹' s)) :

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

theorem Set.subsingleton_range {β : Type u_2} {α : Sort u_6} [Subsingleton α] (f : αβ) :
theorem Set.Nontrivial.preimage {α : Type u_1} {β : Type u_2} {s : Set β} (hs : Set.Nontrivial s) {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 : Set.Nontrivial s) {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 : 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 : Function.Injective f) (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.Injective.preimage_image {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) (s : Set α) :
f ⁻¹' (f '' s) = s
theorem Function.Injective.subsingleton_image_iff {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) {s : Set α} :
theorem Function.Surjective.image_preimage {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Surjective f) (s : Set β) :
f '' (f ⁻¹' s) = s
theorem Function.Surjective.image_surjective {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Surjective f) :
@[simp]
theorem Function.Surjective.nonempty_preimage {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Surjective f) {s : Set β} :
theorem Function.Injective.image_injective {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) :
theorem Function.Surjective.preimage_subset_preimage_iff {α : Type u_3} {β : Type u_2} {f : αβ} {s : Set β} {t : Set β} (hf : Function.Surjective f) :
f ⁻¹' s f ⁻¹' t s t
theorem Function.Surjective.range_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} {f : ιι'} (hf : Function.Surjective f) (g : ι'α) :
theorem Function.Injective.mem_range_iff_exists_unique {α : Sort u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) {b : β} :
b Set.range f ∃! (a : α), f a = b
theorem Function.Injective.exists_unique_of_mem_range {α : Sort u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) {b : β} (hb : b Set.range f) :
∃! (a : α), f a = b
theorem Function.Injective.compl_image_eq {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.Injective f) (s : Set α) :
(f '' s) = f '' s (Set.range f)
theorem Function.LeftInverse.image_image {α : Type u_2} {β : Type u_3} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (s : Set α) :
g '' (f '' s) = s
theorem Function.LeftInverse.preimage_preimage {α : Type u_2} {β : Type u_3} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (s : Set α) :
f ⁻¹' (g ⁻¹' s) = s
@[simp]
theorem EquivLike.range_comp {ι : Sort u_3} {ι' : Sort u_4} {E : Type u_1} [EquivLike E ι ι'] {α : Type u_2} (f : ι'α) (e : E) :

Image and preimage on subtypes #

theorem Subtype.coe_image {α : Type u_1} {p : αProp} {s : Set (Subtype p)} :
Subtype.val '' s = {x : α | ∃ (h : p x), { 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 : s | 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 → α, then the inferred implicit arguments of (↑) are ↑α (fun x ↦ x ∈ 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) = s t
theorem Subtype.image_preimage_val {α : Type u_1} (s : Set α) (t : Set α) :
Subtype.val '' (Subtype.val ⁻¹' t) = s t
theorem Subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} :
Subtype.val ⁻¹' t = Subtype.val ⁻¹' u s t = s u
theorem Subtype.preimage_coe_self_inter {α : Type u_1} (s : Set α) (t : Set α) :
Subtype.val ⁻¹' (s t) = Subtype.val ⁻¹' t
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 s t = s u
theorem Subtype.exists_set_subtype {α : Type u_1} {t : Set α} (p : Set αProp) :
(∃ (s : Set t), p (Subtype.val '' 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)) st, p 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 : s) => x) ⁻¹' s =

Images and preimages on Option #

theorem Option.injective_iff {α : Type u_1} {β : Type u_2} {f : Option αβ} :
theorem Option.range_eq {α : Type u_1} {β : Type u_2} (f : Option αβ) :
Set.range f = insert (f none) (Set.range (f some))
theorem WithBot.range_eq {α : Type u_1} {β : Type u_2} (f : WithBot αβ) :
Set.range f = insert (f ) (Set.range (f WithBot.some))
theorem WithTop.range_eq {α : Type u_1} {β : Type u_2} (f : WithTop αβ) :
Set.range 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]
@[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 : Function.Bijective f) {s : Set β} {t : Set α} :
f ⁻¹' s = t s = f '' t
theorem Set.eq_preimage_iff_image_eq {α : Type u} {β : Type v} {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 : Set β} {t : Set β} (h : Disjoint s 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 : bs, ct, 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 : Set α} {t : Set α} (hd : Disjoint s t) :
Disjoint (f '' s) (f '' t)
theorem Disjoint.of_image {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} (h : Disjoint (f '' s) (f '' t)) :
@[simp]
theorem Set.disjoint_image_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set α} (hf : Function.Injective f) :
Disjoint (f '' s) (f '' t) Disjoint s t
theorem Disjoint.of_preimage {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Surjective f) {s : Set β} {t : Set β} (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) :
@[simp]
theorem Set.disjoint_preimage_iff {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Surjective f) {s : Set β} {t : Set β} :
theorem Set.preimage_eq_empty {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} (h : Disjoint s (Set.range f)) :
theorem Set.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
theorem sigma_mk_preimage_image' {α : Type u_1} {β : αType u_2} {i : α} {j : α} {s : Set (β i)} (h : i j) :
theorem sigma_mk_preimage_image_eq_self {α : Type u_1} {β : αType u_2} {i : α} {s : Set (β i)} :