Images and preimages of sets

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)

Notation

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

• f '' s for Set.image f s

Tags

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

Inverse image

@[simp]

theorem Set.preimage_empty {α : Type u_1} {β : Type u_2} {f : α → β} : 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 t : Set β} (h : s ⊆ t) : f ⁻¹' s ⊆ f ⁻¹' t

@[simp]

theorem Set.preimage_univ {α : Type u_1} {β : Type u_2} {f : α → β} : f ⁻¹' univ = univ

theorem Set.subset_preimage_univ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : s ⊆ f ⁻¹' univ

@[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 β} : f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ

@[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_symmDiff {α : Type u_1} {β : Type u_2} {f : α → β} (s t : Set β) : f ⁻¹' symmDiff s t = symmDiff (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_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} : preimage id = 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_1} {β : Type u_2} {b : β} {s : Set β} (h : b ∈ s) : (fun (x : α) => b) ⁻¹' s = univ

@[simp]

theorem Set.preimage_const_of_notMem {α : Type u_1} {β : Type u_2} {b : β} {s : Set β} (h : b ∉ s) : (fun (x : α) => b) ⁻¹' s = ∅

@[deprecated Set.preimage_const_of_notMem (since := "2025-05-23")]

theorem Set.preimage_const_of_not_mem {α : Type u_1} {β : Type u_2} {b : β} {s : Set β} (h : b ∉ s) : (fun (x : α) => b) ⁻¹' s = ∅

Alias of Set.preimage_const_of_notMem.

theorem Set.preimage_const {α : Type u_1} {β : Type u_2} (b : β) (s : Set β) [Decidable (b ∈ s)] : (fun (x : α) => b) ⁻¹' s = if b ∈ s then univ else ∅

theorem Set.exists_eq_const_of_preimage_singleton {α : Type u_1} {β : Type u_2} [Nonempty β] {f : α → β} (hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = 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 : β → γ} : preimage (g ∘ f) = preimage f ∘ preimage g

theorem Set.preimage_iterate_eq {α : Type u_1} {f : α → α} {n : ℕ} : preimage f^[n] = (preimage 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), ⟨x, h⟩ ∈ s ↔ x ∈ t

theorem Set.nonempty_of_nonempty_preimage {α : Type u_1} {β : Type u_2} {s : Set β} {f : α → β} (hf : (f ⁻¹' s).Nonempty) : s.Nonempty

@[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 u v : Set α} (hsuv : s ⊆ u ∪ v) (H : s ∩ (u ∩ v) = ∅) : Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ

theorem Set.preimage_subset {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} {t : Set α} (hs : s ⊆ f '' t) (hf : InjOn f (f ⁻¹' s)) : f ⁻¹' s ⊆ t

Image of a set under a function

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 : Injective f) {s : Set α} {a : α} : f a ∈ f '' s ↔ a ∈ s

theorem Set.preimage_subset_of_surjOn {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} (hf : Function.Injective f) (h : SurjOn f s t) : f ⁻¹' t ⊆ s

theorem Set.forall_mem_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : β → Prop} : (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

theorem Set.exists_mem_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : β → Prop} : (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x)

theorem Set.image_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α} (h : ∀ 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_mono {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α} (h : s ⊆ t) : f '' s ⊆ f '' t

theorem Set.monotone_image {α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (image f)

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

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 : β → γ} : image (g ∘ f) = image g ∘ image f

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_5} {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 : Semiconj f ga gb) : Semiconj (Set.image f) (Set.image ga) (Set.image gb)

theorem Function.Commute.set_image {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Function.Commute (Set.image f) (Set.image g)

@[deprecated Set.image_mono (since := "2025-08-01")]

theorem Set.image_subset {α : Type u_1} {β : Type u_2} {a b : Set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f '' b

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 : α → β) : 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 ∈ t, ∀ 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_5} {f : ι → β} (H : Function.Surjective f) : f '' univ = 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 : s.Nonempty) (a : β) : (fun (x : α) => a) '' s = {a}

@[simp]

theorem Set.image_eq_empty {α : Type u_5} {β : Type u_6} {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} : 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 : ℕ} : image f^[n] = (image 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.range_inter_ssubset_iff_preimage_ssubset {α : Type u_1} {β : Type u_2} {f : α → β} {s s' : Set β} : range f ∩ s ⊂ range f ∩ s' ↔ f ⁻¹' s ⊂ f ⁻¹' 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) : image f = preimage g

theorem Function.Involutive.image_eq_preimage {α : Type u_1} {f : α → α} (hf : Involutive f) : Set.image f = Set.preimage 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 t : Set α) : f '' s \ f '' t ⊆ f '' (s \ t)

theorem Set.subset_image_symmDiff {α : Type u_1} {β : Type u_2} {f : α → β} {s 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 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 t : Set α) : f '' symmDiff s t = symmDiff (f '' s) (f '' t)

theorem Set.Nonempty.image {α : Type u_1} {β : Type u_2} (f : α → β) {s : Set α} : s.Nonempty → (f '' s).Nonempty

theorem Set.Nonempty.of_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : (f '' s).Nonempty → s.Nonempty

@[simp]

theorem Set.image_nonempty {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : (f '' s).Nonempty ↔ s.Nonempty

theorem Set.Nonempty.preimage {α : Type u_1} {β : Type u_2} {s : Set β} (hs : s.Nonempty) {f : α → β} (hf : Function.Surjective f) : (f ⁻¹' s).Nonempty

instance Set.instNonemptyElemImage {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) [Nonempty ↑s] : Nonempty ↑(f '' 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_univ {α : Type u_1} {β : Type u_2} {f : α → β} : f ⁻¹' (f '' univ) = univ

@[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 : s.Nonempty) (t : Set β) (a : β) : s ⊆ (fun (x : α) => a) ⁻¹' t ↔ a ∈ t

@[simp]

theorem Set.preimage_injective {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Injective (preimage f) ↔ Function.Surjective f

@[simp]

theorem Set.preimage_surjective {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective (preimage f) ↔ Function.Injective f

@[simp]

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.disjoint_image_left {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)

theorem Set.disjoint_image_right {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s

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} : image compl = preimage compl

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 ∈ 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.subset_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : t ⊆ f '' s ↔ ∃ u ⊆ s, f '' u = t

@[simp]

theorem Set.exists_subset_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : Set β → Prop} : (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)

@[simp]

theorem Set.forall_subset_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : Set β → Prop} : (∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' 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 : 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 ∘ imageFactorization f s = f ∘ Subtype.val

theorem Set.imageFactorization_surjective {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : Function.Surjective (imageFactorization f s)

@[deprecated Set.imageFactorization_surjective (since := "2025-08-18")]

theorem Set.surjective_onto_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : Function.Surjective (imageFactorization f s)

Alias of Set.imageFactorization_surjective.

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 : α) : 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

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

theorem Set.disjoint_powerset_insert {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s) : Disjoint (𝒫 s) (insert a '' 𝒫 s)

theorem Set.powerset_insert_injOn {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s) : InjOn (insert a) (𝒫 s)

Lemmas about range of a function.

theorem Set.forall_mem_range {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop} : (∀ a ∈ range f, p a) ↔ ∀ (i : ι), p (f i)

theorem Set.forall_subtype_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : ↑(range f) → Prop} : (∀ (a : ↑(range f)), p a) ↔ ∀ (i : ι), p ⟨f i, ⋯⟩

theorem Set.exists_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop} : (∃ a ∈ range f, p a) ↔ ∃ (i : ι), p (f i)

theorem Set.exists_subtype_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : ↑(range f) → Prop} : (∃ (a : ↑(range f)), p a) ↔ ∃ (i : ι), p ⟨f i, ⋯⟩

theorem Set.range_eq_univ {α : Type u_1} {ι : Sort u_4} {f : ι → α} : range f = univ ↔ Function.Surjective f

theorem Function.Surjective.range_eq {α : Type u_1} {ι : Sort u_4} {f : ι → α} : Surjective f → Set.range f = Set.univ

Alias of the reverse direction of Set.range_eq_univ.

@[simp]

theorem Set.subset_range_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Surjective f) (s : Set β) : s ⊆ range f

@[simp]

theorem Set.image_univ {α : Type u_1} {β : Type u_2} {f : α → β} : f '' univ = range f

theorem Set.image_compl_eq_range_diff_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (s : Set α) : f '' sᶜ = range f \ f '' s

theorem Set.range_diff_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (s : Set α) : range f \ f '' s = f '' sᶜ

Alias of Set.image_compl_eq_range_sdiff_image.

@[simp]

theorem Set.preimage_eq_univ_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f ⁻¹' s = univ ↔ range f ⊆ s

theorem Set.image_subset_range {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : f '' s ⊆ range f

theorem Set.mem_range_of_mem_image {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) {x : β} (h : x ∈ f '' s) : x ∈ range f

theorem Nat.mem_range_succ (i : ℕ) : i ∈ Set.range succ ↔ 0 < i

theorem Set.Nonempty.preimage' {α : Type u_1} {β : Type u_2} {s : Set β} (hs : s.Nonempty) {f : α → β} (hf : s ⊆ range f) : (f ⁻¹' s).Nonempty

theorem Set.range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α) : range (g ∘ f) = g '' range f

theorem Set.range_comp' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α) : (range fun (x : ι) => g (f x)) = g '' range f

Variant of range_comp using a lambda instead of function composition.

theorem Set.range_subset_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : 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 : β → γ} : range f ⊆ range g ↔ ∃ (h : α → β), f = g ∘ h

theorem Set.range_eq_iff {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ (a : α), f a = b

theorem Set.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : range (g ∘ f) ⊆ range g

theorem Set.range_nonempty_iff_nonempty {α : Type u_1} {ι : Sort u_4} {f : ι → α} : (range f).Nonempty ↔ Nonempty ι

theorem Set.range_nonempty {α : Type u_1} {ι : Sort u_4} [h : Nonempty ι] (f : ι → α) : (range f).Nonempty

@[simp]

theorem Set.range_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} : range f = ∅ ↔ IsEmpty ι

theorem Set.range_eq_empty {α : Type u_1} {ι : Sort u_4} [IsEmpty ι] (f : ι → α) : range f = ∅

@[simp]

theorem Set.range_eq_singleton_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} [Nonempty ι] {y : α} : range f = {y} ↔ ∀ (x : ι), f x = y

theorem Set.range_eq_singleton {α : Type u_1} {ι : Sort u_4} {f : ι → α} [Nonempty ι] {y : α} (hy : ∀ (x : ι), f x = y) : range f = {y}

instance Set.instNonemptyRange {α : Type u_1} {ι : Sort u_4} [Nonempty ι] (f : ι → α) : Nonempty ↑(range f)

@[simp]

theorem Set.image_union_image_compl_eq_range {α : Type u_1} {β : Type u_2} {s : Set α} (f : α → β) : f '' s ∪ f '' sᶜ = range f

theorem Set.insert_image_compl_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : insert (f x) (f '' {x}ᶜ) = range f

theorem Set.image_preimage_eq_range_inter {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = range f ∩ t

theorem Set.image_preimage_eq_inter_range {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = t ∩ range f

theorem Set.image_preimage_eq_of_subset {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} (hs : s ⊆ 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 ⊆ range f

theorem Set.subset_range_iff_exists_image_eq {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : s ⊆ range f ↔ ∃ (t : Set α), f '' t = s

theorem Set.range_image {α : Type u_1} {β : Type u_2} (f : α → β) : range (image f) = 𝒫 range f

@[simp]

theorem Set.exists_subset_range_and_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : Set β → Prop} : (∃ s ⊆ range f, p s) ↔ ∃ (s : Set α), p (f '' s)

@[simp]

theorem Set.forall_subset_range_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : Set β → Prop} : (∀ s ⊆ range f, p s) ↔ ∀ (s : Set α), p (f '' s)

@[simp]

theorem Set.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {s t : Set α} {f : β → α} (hs : s ⊆ range f) : f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

theorem Set.preimage_eq_preimage' {α : Type u_1} {β : Type u_2} {s t : Set α} {f : β → α} (hs : s ⊆ range f) (ht : t ⊆ range f) : f ⁻¹' s = f ⁻¹' t ↔ s = t

theorem Set.preimage_inter_range {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f ⁻¹' (s ∩ range f) = f ⁻¹' s

theorem Set.preimage_range_inter {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f ⁻¹' (range 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} : range id = univ

@[simp]

theorem Set.range_id' {α : Type u_1} : (range fun (x : α) => x) = univ

@[simp]

theorem Prod.range_fst {α : Type u_1} {β : Type u_2} [Nonempty β] : Set.range fst = Set.univ

@[simp]

theorem Prod.range_snd {α : Type u_1} {β : Type u_2} [Nonempty α] : Set.range snd = Set.univ

@[simp]

theorem Set.range_eval {ι : Sort u_4} {α : ι → Type u_5} [∀ (i : ι), Nonempty (α i)] (i : ι) : range (Function.eval i) = univ

theorem Set.range_inl {α : Type u_1} {β : Type u_2} : range Sum.inl = {x : α ⊕ β | x.isLeft = true}

theorem Set.range_inr {α : Type u_1} {β : Type u_2} : range Sum.inr = {x : α ⊕ β | x.isRight = true}

theorem Set.isCompl_range_inl_range_inr {α : Type u_1} {β : Type u_2} : IsCompl (range Sum.inl) (range Sum.inr)

@[simp]

theorem Set.range_inl_union_range_inr {α : Type u_1} {β : Type u_2} : range Sum.inl ∪ range Sum.inr = univ

@[simp]

theorem Set.range_inl_inter_range_inr {α : Type u_1} {β : Type u_2} : range Sum.inl ∩ range Sum.inr = ∅

@[simp]

theorem Set.range_inr_union_range_inl {α : Type u_1} {β : Type u_2} : range Sum.inr ∪ range Sum.inl = univ

@[simp]

theorem Set.range_inr_inter_range_inl {α : Type u_1} {β : Type u_2} : range Sum.inr ∩ 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 ⁻¹' range Sum.inr = ∅

@[simp]

theorem Set.preimage_inr_range_inl {α : Type u_1} {β : Type u_2} : Sum.inr ⁻¹' range Sum.inl = ∅

@[simp]

theorem Set.compl_range_inl {α : Type u_1} {β : Type u_2} : (range Sum.inl)ᶜ = range Sum.inr

@[simp]

theorem Set.compl_range_inr {α : Type u_1} {β : Type u_2} : (range Sum.inr)ᶜ = range Sum.inl

theorem Set.preimage_sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set γ) (f : α → γ) (g : β → γ) : Sum.elim f g ⁻¹' s = Sum.inl '' (f ⁻¹' s) ∪ Sum.inr '' (g ⁻¹' s)

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

theorem Set.image_sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set (α ⊕ β)) (f : α → γ) (g : β → γ) : Sum.elim f g '' s = f '' (Sum.inl ⁻¹' s) ∪ g '' (Sum.inr ⁻¹' s)

@[simp]

theorem Set.range_quot_mk {α : Type u_1} (r : α → α → Prop) : range (Quot.mk r) = 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) : range (Quot.lift f hf) = range f

@[simp]

theorem Set.range_quotient_mk {α : Type u_1} {s : Setoid α} : range (Quotient.mk s) = 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) : range (Quotient.lift f hf) = range f

@[simp]

theorem Set.range_quotient_mk' {α : Type u_1} {s : Setoid α} : range Quotient.mk' = univ

theorem Set.Quotient.range_mk'' {α : Type u_1} {sa : Setoid α} : range Quotient.mk'' = univ

@[simp]

theorem Set.range_quotient_lift_on' {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : Setoid ι} (hf : ∀ (a b : ι), s a b → f a = f b) : (range fun (x : Quotient s) => x.liftOn' f hf) = 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 α) => ∀ x ∈ s, p x

theorem Set.range_const_subset {α : Type u_1} {ι : Sort u_4} {c : α} : (range fun (x : ι) => c) ⊆ {c}

@[simp]

theorem Set.range_const {α : Type u_1} {ι : Sort u_4} [Nonempty ι] {c : α} : (range fun (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)) : range (Subtype.map f h) = Subtype.val ⁻¹' (f '' {x : α | p x})

theorem Set.image_swap_eq_preimage_swap {α : Type u_1} {β : Type u_2} : image Prod.swap = preimage Prod.swap

theorem Set.preimage_singleton_nonempty {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} : (f ⁻¹' {y}).Nonempty ↔ y ∈ range f

theorem Set.preimage_singleton_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} : f ⁻¹' {y} = ∅ ↔ y ∉ range f

theorem Set.range_subset_singleton {α : Type u_1} {ι : Sort u_4} {f : ι → α} {x : α} : range f ⊆ {x} ↔ f = Function.const ι x

theorem Set.image_compl_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f '' (f ⁻¹' s)ᶜ = range f \ s

theorem Set.rangeFactorization_eq {β : Type u_2} {ι : Sort u_4} {f : ι → β} : Subtype.val ∘ rangeFactorization f = f

@[simp]

theorem Set.rangeFactorization_coe {β : Type u_2} {ι : Sort u_4} (f : ι → β) (a : ι) : ↑(rangeFactorization f a) = f a

@[simp]

theorem Set.coe_comp_rangeFactorization {β : Type u_2} {ι : Sort u_4} (f : ι → β) : Subtype.val ∘ rangeFactorization f = f

theorem Set.rangeFactorization_surjective {α : Type u_1} {ι : Sort u_4} {f : ι → α} : Function.Surjective (rangeFactorization f)

@[deprecated Set.rangeFactorization_surjective (since := "2025-08-18")]

theorem Set.surjective_onto_range {α : Type u_1} {ι : Sort u_4} {f : ι → α} : Function.Surjective (rangeFactorization f)

Alias of Set.rangeFactorization_surjective.

theorem Set.image_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : f '' s = 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 ∘ inl) ∪ Set.range (f ∘ inr)

@[simp]

theorem Set.Sum.elim_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) : range (Sum.elim f g) = range f ∪ range g

theorem Set.range_ite_subset' {α : Type u_1} {β : Type u_2} {p : Prop} [Decidable p] {f g : α → β} : range (if p then f else g) ⊆ range f ∪ range g

theorem Set.range_ite_subset {α : Type u_1} {β : Type u_2} {p : α → Prop} [DecidablePred p] {f g : α → β} : (range fun (x : α) => if p x then f x else g x) ⊆ range f ∪ range g

@[simp]

theorem Set.preimage_range {α : Type u_1} {β : Type u_2} (f : α → β) : f ⁻¹' range f = univ

theorem Set.range_unique {α : Type u_1} {ι : Sort u_4} {f : ι → α} [h : Unique ι] : 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 α) : range f \ f '' s ⊆ f '' sᶜ

@[simp]

theorem Set.range_inclusion {α : Type u_1} {s t : Set α} (h : s ⊆ t) : range (inclusion h) = {x : ↑t | ↑x ∈ s}

theorem Set.leftInverse_rangeSplitting {α : Type u_1} {β : Type u_2} (f : α → β) : Function.LeftInverse (rangeFactorization f) (rangeSplitting f)

theorem Set.rangeSplitting_injective {α : Type u_1} {β : Type u_2} (f : α → β) : Function.Injective (rangeSplitting f)

theorem Set.rightInverse_rangeSplitting {α : Type u_1} {β : Type u_2} {f : α → β} (h : Function.Injective f) : Function.RightInverse (rangeFactorization f) (rangeSplitting f)

theorem Set.preimage_rangeSplitting {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : preimage (rangeSplitting f) = image (rangeFactorization f)

theorem Set.isCompl_range_some_none (α : Type u_5) : IsCompl (range some) {none}

@[simp]

theorem Set.compl_range_some (α : Type u_5) : (range some)ᶜ = {none}

@[simp]

theorem Set.range_some_inter_none (α : Type u_5) : range some ∩ {none} = ∅

theorem Set.range_some_union_none (α : Type u_5) : range some ∪ {none} = univ

@[simp]

theorem Set.insert_none_range_some (α : Type u_5) : insert none (range some) = univ

theorem Set.image_of_range_union_range_eq_univ {α : Type u_5} {β : Type u_6} {γ : Type u_7} {γ' : Type u_8} {δ : Type u_9} {δ' : Type u_10} {h : β → α} {f : γ → β} {f₁ : γ' → α} {f₂ : γ → γ'} {g : δ → β} {g₁ : δ' → α} {g₂ : δ → δ'} (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂) (hfg : range f ∪ range g = univ) (s : Set β) : h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s))

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

The image of a subsingleton is a subsingleton.

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

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) : 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) : s.Subsingleton

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_5} [Subsingleton α] (f : α → β) : (range f).Subsingleton

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

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

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

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

theorem Set.Nontrivial.image_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hs : s.Nontrivial) (hf : InjOn f s) : (f '' s).Nontrivial

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

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

@[simp]

theorem Set.image_nontrivial {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hf : Function.Injective f) : (f '' s).Nontrivial ↔ s.Nontrivial

@[simp]

theorem Set.InjOn.image_nontrivial_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hf : InjOn f s) : (f '' s).Nontrivial ↔ s.Nontrivial

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

theorem Function.Injective.preimage_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) (s : Set α) : f ⁻¹' (f '' s) = s

theorem Function.Injective.preimage_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) : Surjective (Set.preimage f)

theorem Function.Injective.subsingleton_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) {s : Set α} : (f '' s).Subsingleton ↔ s.Subsingleton

theorem Function.Surjective.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) (s : Set β) : f '' (f ⁻¹' s) = s

theorem Function.Surjective.image_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) : Surjective (Set.image f)

@[simp]

theorem Function.Surjective.nonempty_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) {s : Set β} : (f ⁻¹' s).Nonempty ↔ s.Nonempty

theorem Function.Injective.image_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) : Injective (Set.image f)

theorem Function.Injective.image_strictMono {α : Type u_1} {β : Type u_2} {f : α → β} (inj : Injective f) : StrictMono (Set.image f)

theorem Function.Surjective.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β} (hf : Surjective f) : f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

theorem Function.Surjective.range_comp {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} {f : ι → ι'} (hf : Surjective f) (g : ι' → α) : Set.range (g ∘ f) = Set.range g

theorem Function.Injective.mem_range_iff_existsUnique {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) {b : β} : b ∈ Set.range f ↔ ∃! a : α, f a = b

theorem Function.Injective.existsUnique_of_mem_range {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) {b : β} : b ∈ Set.range f → ∃! a : α, f a = b

Alias of the forward direction of Function.Injective.mem_range_iff_existsUnique.

theorem Function.Injective.compl_image_eq {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) (s : Set α) : (f '' s)ᶜ = f '' sᶜ ∪ (Set.range f)ᶜ

theorem Function.LeftInverse.image_image {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : LeftInverse g f) (s : Set α) : g '' (f '' s) = s

theorem Function.LeftInverse.preimage_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : LeftInverse g f) (s : Set α) : f ⁻¹' (g ⁻¹' s) = s

theorem Function.Involutive.preimage {α : Type u_1} {f : α → α} (hf : Involutive f) : Involutive (Set.preimage f)

@[simp]

theorem EquivLike.range_comp {ι : Sort u_1} {ι' : Sort u_2} {E : Type u_3} [EquivLike E ι ι'] {α : Type u_4} (f : ι' → α) (e : E) : Set.range (f ∘ ⇑e) = Set.range f

Image and preimage on subtypes

theorem Subtype.coe_image {α : Type u_1} {p : α → Prop} {s : Set (Subtype p)} : val '' s = {x : α | ∃ (h : p x), ⟨x, h⟩ ∈ s}

@[simp]

theorem Subtype.coe_image_of_subset {α : Type u_1} {s t : Set α} (h : t ⊆ s) : val '' {x : ↑s | ↑x ∈ t} = t

theorem Subtype.range_coe {α : Type u_1} {s : Set α} : Set.range val = s

theorem Subtype.range_val {α : Type u_1} {s : Set α} : Set.range 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 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 α) : val ⁻¹' s = Set.univ

theorem Subtype.range_val_subtype {α : Type u_1} {p : α → Prop} : Set.range val = {x : α | p x}

theorem Subtype.coe_image_subset {α : Type u_1} (s : Set α) (t : Set ↑s) : val '' t ⊆ s

theorem Subtype.coe_image_univ {α : Type u_1} (s : Set α) : val '' Set.univ = s

@[simp]

theorem Subtype.image_preimage_coe {α : Type u_1} (s t : Set α) : val '' (val ⁻¹' t) = s ∩ t

theorem Subtype.image_preimage_val {α : Type u_1} (s t : Set α) : val '' (val ⁻¹' t) = s ∩ t

theorem Subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s t u : Set α} : val ⁻¹' t = val ⁻¹' u ↔ s ∩ t = s ∩ u

theorem Subtype.preimage_coe_self_inter {α : Type u_1} (s t : Set α) : val ⁻¹' (s ∩ t) = val ⁻¹' t

theorem Subtype.preimage_coe_inter_self {α : Type u_1} (s t : Set α) : val ⁻¹' (t ∩ s) = val ⁻¹' t

theorem Subtype.preimage_val_eq_preimage_val_iff {α : Type u_1} (s t u : Set α) : val ⁻¹' t = val ⁻¹' u ↔ s ∩ t = s ∩ u

theorem Subtype.preimage_val_subset_preimage_val_iff {α : Type u_1} (s t u : Set α) : val ⁻¹' t ⊆ val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u

theorem Subtype.exists_set_subtype {α : Type u_1} {t : Set α} (p : Set α → Prop) : (∃ (s : Set ↑t), p (val '' s)) ↔ ∃ s ⊆ t, p s

theorem Subtype.forall_set_subtype {α : Type u_1} {t : Set α} (p : Set α → Prop) : (∀ (s : Set ↑t), p (val '' s)) ↔ ∀ s ⊆ t, p s

theorem Subtype.preimage_coe_nonempty {α : Type u_1} {s t : Set α} : (val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty

theorem Subtype.preimage_coe_eq_empty {α : Type u_1} {s t : Set α} : val ⁻¹' t = ∅ ↔ s ∩ t = ∅

theorem Subtype.preimage_coe_compl {α : Type u_1} (s : Set α) : 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 α → β} : Function.Injective f ↔ Function.Injective (f ∘ some) ∧ f none ∉ Set.range (f ∘ some)

theorem Option.range_eq {α : Type u_1} {β : Type u_2} (f : Option α → β) : Set.range f = insert (f none) (Set.range (f ∘ some))

Injectivity and surjectivity lemmas for image and preimage

@[simp]

theorem Set.image_surjective {α : Type u} {β : Type v} {f : α → β} : Function.Surjective (image f) ↔ Function.Surjective f

@[simp]

theorem Set.image_injective {α : Type u} {β : Type v} {f : α → β} : Function.Injective (image f) ↔ Function.Injective 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 t : Set β} (h : Disjoint s t) : Disjoint (f ⁻¹' s) (f ⁻¹' t)

theorem Codisjoint.preimage {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β} (h : Codisjoint s t) : Codisjoint (f ⁻¹' s) (f ⁻¹' t)

theorem IsCompl.preimage {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β} (h : IsCompl s t) : IsCompl (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 ∈ s, ∀ 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 : Disjoint s 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)) : Disjoint s t

@[simp]

theorem Set.disjoint_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s 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 t : Set β} (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) : Disjoint s t

@[simp]

theorem Set.disjoint_preimage_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) {s t : Set β} : Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t

theorem Set.preimage_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} (h : Disjoint s (range f)) : f ⁻¹' s = ∅

theorem Set.preimage_eq_empty_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (range f)

@[simp]

theorem Set.disjoint_image_inl_image_inr {α : Type u_1} {β : Type u_2} {u : Set α} {v : Set β} : Disjoint (Sum.inl '' u) (Sum.inr '' v)

@[simp]

theorem Set.disjoint_range_inl_image_inr {α : Type u_1} {β : Type u_2} {v : Set β} : Disjoint (range Sum.inl) (Sum.inr '' v)

@[simp]

theorem Set.disjoint_image_inl_range_inr {α : Type u_1} {β : Type u_2} {u : Set α} : Disjoint (Sum.inl '' u) (range Sum.inr)

theorem sigma_mk_preimage_image' {α : Type u_1} {β : α → Type u_2} {i j : α} {s : Set (β i)} (h : i ≠ j) : Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅

theorem sigma_mk_preimage_image_eq_self {α : Type u_1} {β : α → Type u_2} {i : α} {s : Set (β i)} : Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s