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

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

• f ⁻¹' s = {x | f x ∈ s}

def Set.«term_⁻¹'_» : Lean.TrailingParserDescr

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

Equations

• Set.«term_⁻¹'_» = Lean.ParserDescr.trailingNode `Set.term_⁻¹'_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹' ") (Lean.ParserDescr.cat `term 81))

@[simp]

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

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

@[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} : Set.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 = Set.univ

@[simp]

theorem Set.preimage_const_of_not_mem {α : Type u_1} {β : Type u_2} {b : β} {s : Set β} (h : ¬b ∈ s) : (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 : β → γ} : Set.preimage (g ∘ f) = Set.preimage f ∘ Set.preimage g

theorem Set.preimage_iterate_eq {α : Type u_1} {f : α → α} {n : ℕ} : Set.preimage f^[n] = (Set.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), { 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)) : Set.Nonempty 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_6} {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

def Set.term_''_ : Lean.TrailingParserDescr

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

Equations

• Set.term_''_ = Lean.ParserDescr.trailingNode `Set.term_''_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " '' ") (Lean.ParserDescr.cat `term 81))

theorem Set.mem_image_iff_bex {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {y : β} : y ∈ f '' s ↔ ∃ x x_1, f x = y

@[simp]

theorem Set.mem_image {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (y : β) : y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y

theorem Set.image_eta {α : Type u_1} {β : Type u_2} {s : Set α} (f : α → β) : f '' s = (fun x => f x) '' s

theorem Set.mem_image_of_mem {α : Type u_1} {β : Type u_2} (f : α → β) {x : α} {a : Set α} (h : x ∈ a) : f x ∈ f '' a

theorem Function.Injective.mem_set_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : 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 : β) : y ∈ f '' s → p y

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

theorem Set.mem_image_elim {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {C : β → Prop} (h : ∀ (x : α), x ∈ 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) = (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) : Function.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)

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 : α → β} : Monotone (Set.image 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 : α → β) : f '' ∅ = ∅

theorem Set.image_inter_subset {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set α) : f '' (s ∩ t) ⊆ f '' s ∩ f '' t

theorem Set.image_inter_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set α} (h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ 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 : 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' {α : Type u_1} (s : Set α) : (fun x => x) '' s = s

A variant of image_id

theorem Set.image_id {α : Type u_1} (s : Set α) : id '' s = s

theorem Set.compl_compl_image {α : Type u_1} [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) : Set.image f = Set.preimage g

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 α} : (f '' s) ∆ (f '' t) ⊆ f '' 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 '' s ∆ t = (f '' s) ∆ (f '' t)

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

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

@[simp]

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

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

instance Set.instNonemptyElemImage {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) [Nonempty ↑s] : Nonempty ↑(f '' s)

Equations

• @Set.instNonemptyElemImage = @Set.instNonemptyElemImage.proof_1

@[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.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 β} : Set.Nonempty (f '' s ∩ t) ↔ Set.Nonempty (s ∩ f ⁻¹' t)

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

theorem Set.compl_image_set_of {α : Type u_1} {p : Set α → Prop} : compl '' {s | p s} = {s | p sᶜ}

theorem Set.inter_preimage_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β) : s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)

theorem Set.union_preimage_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β) : s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)

theorem Set.subset_image_union {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) : f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t

theorem Set.preimage_subset_iff {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {f : α → β} : f ⁻¹' B ⊆ A ↔ ∀ (a : α), f a ∈ B → a ∈ 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.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 | (g x.1, g x.2) ∈ r} = (fun a => (Quotient.mk s a.1, Quotient.mk s 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, P ↑a) ↔ ∃ a, P (f ↑a)

def Set.imageFactorization {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : ↑s → ↑(f '' s)

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

Equations

• Set.imageFactorization f s p = { val := f ↑p, property := (_ : f ↑p ∈ f '' s) }

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 α} : Function.Surjective (Set.imageFactorization f s)

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.

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

• Set.range f = {x | ∃ y, f y = x}

@[simp]

theorem Set.mem_range {α : Type u_1} {ι : Sort u_4} {f : ι → α} {x : α} : x ∈ Set.range f ↔ ∃ y, f y = x

theorem Set.mem_range_self {α : Type u_1} {ι : Sort u_4} {f : ι → α} (i : ι) : f i ∈ Set.range f

theorem Set.forall_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop} : (∀ (a : α), a ∈ Set.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, 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, 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, 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 : ι → α} : Set.range f = Set.univ ↔ Function.Surjective f

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

Alias of the reverse direction of Set.range_iff_surjective.

@[simp]

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

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

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

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

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

theorem Set.range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α) : Set.range (g ∘ f) = g '' Set.range 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) ∧ ∀ (b : β), b ∈ s → ∃ a, f a = b

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

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

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

@[simp]

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

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

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

Equations

• @Set.instNonemptyRange = @Set.instNonemptyRange.proof_1

@[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_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, f '' t = s

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

@[simp]

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

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

theorem Set.forall_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.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 β} : f ⁻¹' (s ∩ Set.range f) = f ⁻¹' s

theorem Set.preimage_range_inter {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f ⁻¹' (Set.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} : 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 {ι : Type u_6} {α : ι → Type u_7} [∀ (i : ι), Nonempty (α i)] (i : ι) : Set.range (Function.eval i) = Set.univ

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 y → f x = f y) : Set.range (Quot.lift f hf) = Set.range f

@[simp]

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

@[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 b → f a = f b) : (Set.range fun x => 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 x_1 => x '' x_1) c) fun s => ∀ (x : α), x ∈ s → p x

Equations

• @Set.canLift = @Set.canLift.proof_1

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 x → q (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 : β} : Set.Nonempty (f ⁻¹' {y}) ↔ y ∈ Set.range f

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

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

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

def Set.rangeFactorization {β : Type u_2} {ι : Sort u_4} (f : ι → β) : ι → ↑(Set.range f)

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

Equations

• Set.rangeFactorization f i = { val := f i, property := (_ : f i ∈ Set.range f) }

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 : ι) : ↑(Set.rangeFactorization f a) = 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 : ι → α} : Function.Surjective (Set.rangeFactorization f)

theorem Set.image_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : f '' s = Set.range fun x => f ↑x

theorem Sum.range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ) : Set.range f = 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 : β → γ) : Set.range (Sum.elim f g) = Set.range f ∪ Set.range 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 | ↑x ∈ s}

noncomputable def Set.rangeSplitting {α : Type u_1} {β : Type u_2} (f : α → β) : ↑(Set.range f) → α

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

Equations

• Set.rangeSplitting f x = Exists.choose (_ : ↑x ∈ Set.range f)

theorem Set.apply_rangeSplitting {α : Type u_1} {β : Type u_2} (f : α → β) (x : ↑(Set.range f)) : f (Set.rangeSplitting f x) = ↑x

@[simp]

theorem Set.comp_rangeSplitting {α : Type u_1} {β : Type u_2} (f : α → β) : f ∘ Set.rangeSplitting f = Subtype.val

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

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

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

theorem Set.preimage_rangeSplitting {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : Set.preimage (Set.rangeSplitting f) = Set.image (Set.rangeFactorization 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 : α → β) : Set.Subsingleton (f '' s)

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) : Set.Subsingleton (f ⁻¹' s)

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

theorem Set.subsingleton_of_image {α : Type u_6} {β : Type u_7} {f : α → β} (hf : Function.Injective f) (s : Set α) (hs : Set.Subsingleton (f '' s)) : Set.Subsingleton 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_6} {β : Type u_7} {f : α → β} (hf : Function.Surjective f) (s : Set β) (hs : Set.Subsingleton (f ⁻¹' s)) : Set.Subsingleton 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 : α → β) : Set.Subsingleton (Set.range f)

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

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

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

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

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

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.preimage_surjective {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Function.Injective f) : Function.Surjective (Set.preimage f)

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

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) : Function.Surjective (Set.image f)

@[simp]

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

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

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

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

theorem Function.Injective.mem_range_iff_exists_unique {α : Type 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 {α : Type 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

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

@[simp]

theorem EquivLike.range_comp {ι : Sort u_3} {ι' : Sort u_4} {E : Type u_1} [EquivLike E ι ι'] {α : Type u_2} (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)} : Subtype.val '' s = {x | ∃ h, { val := x, property := h } ∈ s}

@[simp]

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

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

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

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

@[simp]

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

We make this the simp lemma instead of range_coe. The reason is that if we write for s : Set α the function (↑) : s → α, 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) = t ∩ s

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

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

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

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

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

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

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 : α → β} : Function.Injective (Set.preimage f) ↔ Function.Surjective f

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Set.disjoint_preimage_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) {s : Set β} {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 (Set.range f)) : f ⁻¹' s = ∅

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

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