data.set.image - mathlib3 docs

source

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}

Instances for set.preimage

source

@[simp]

theorem set.preimage_empty {α : Type u_1} {β : Type u_2} {f : α → β} :

f ⁻¹' ∅ = ∅

source

@[simp]

theorem set.mem_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} {a : α} :

a ∈ f ⁻¹' s ↔ f a ∈ s

source

theorem set.preimage_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) :

f ⁻¹' s = g ⁻¹' s

source

theorem set.preimage_mono {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set β} (h : s ⊆ t) :

f ⁻¹' s ⊆ f ⁻¹' t

source

@[simp]

theorem set.preimage_univ {α : Type u_1} {β : Type u_2} {f : α → β} :

f ⁻¹' set.univ = set.univ

source

theorem set.subset_preimage_univ {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :

s ⊆ f ⁻¹' set.univ

source

@[simp]

theorem set.preimage_inter {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set β} :

f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t

source

@[simp]

theorem set.preimage_union {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set β} :

f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t

source

@[simp]

theorem set.preimage_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :

f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ

source

@[simp]

theorem set.preimage_diff {α : Type u_1} {β : Type u_2} (f : α → β) (s t : set β) :

f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t

source

@[simp]

theorem set.preimage_symm_diff {α : Type u_1} {β : Type u_2} (f : α → β) (s t : set β) :

f ⁻¹' s ∆ t = (f ⁻¹' s) ∆ (f ⁻¹' t)

source

@[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₂)

source

@[simp]

theorem set.preimage_set_of_eq {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : β → α} :

f ⁻¹' {a : α | p a} = {a : β | p (f a)}

source

@[simp]

theorem set.preimage_id_eq {α : Type u_1} :

set.preimage id = id

source

theorem set.preimage_id {α : Type u_1} {s : set α} :

id ⁻¹' s = s

source

@[simp]

theorem set.preimage_id' {α : Type u_1} {s : set α} :

(λ (x : α), x) ⁻¹' s = s

source

@[simp]

theorem set.preimage_const_of_mem {α : Type u_1} {β : Type u_2} {b : β} {s : set β} (h : b ∈ s) :

(λ (x : α), b) ⁻¹' s = set.univ

source

@[simp]

theorem set.preimage_const_of_not_mem {α : Type u_1} {β : Type u_2} {b : β} {s : set β} (h : b ∉ s) :

(λ (x : α), b) ⁻¹' s = ∅

source

theorem set.preimage_const {α : Type u_1} {β : Type u_2} (b : β) (s : set β) [decidable (b ∈ s)] :

(λ (x : α), b) ⁻¹' s = ite (b ∈ s) set.univ ∅

source

theorem set.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {s : set γ} :

g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s)

source

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

source

@[simp]

theorem set.preimage_iterate_eq {α : Type u_1} {f : α → α} {n : ℕ} :

set.preimage f^[n] = (set.preimage f^[n])

source

theorem set.preimage_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set γ} :

f ⁻¹' (g ⁻¹' s) = (λ (x : α), g (f x)) ⁻¹' s

source

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

source

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

s.nonempty

source

@[simp]

theorem set.preimage_singleton_true {α : Type u_1} (p : α → Prop) :

p ⁻¹' {true} = {a : α | p a}

source

@[simp]

theorem set.preimage_singleton_false {α : Type u_1} (p : α → Prop) :

p ⁻¹' {false} = {a : α | ¬p a}

source

theorem set.preimage_subtype_coe_eq_compl {α : Type u_1} {s u v : set α} (hsuv : s ⊆ u ∪ v) (H : s ∩ (u ∩ v) = ∅) :

coe ⁻¹' u = (coe ⁻¹' v)ᶜ

source

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

set β

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

Equations

f '' s = {y : β | ∃ (x : α), x ∈ s ∧ f x = y}

Instances for set.image

Instances for ↥set.image

source

theorem set.mem_image_iff_bex {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {y : β} :

y ∈ f '' s ↔ ∃ (x : α) (_x : x ∈ s), f x = y

source

@[simp]

theorem set.mem_image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (y : β) :

y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y

source

theorem set.image_eta {α : Type u_1} {β : Type u_2} {s : set α} (f : α → β) :

f '' s = (λ (x : α), f x) '' s

source

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

f x ∈ f '' a

source

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

source

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)

source

theorem set.ball_image_of_ball {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {p : β → Prop} (h : ∀ (x : α), x ∈ s → p (f x)) (y : β) (H : y ∈ f '' s) :

p y

source

theorem set.bex_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {p : β → Prop} :

(∃ (y : β) (H : y ∈ f '' s), p y) ↔ ∃ (x : α) (H : x ∈ s), p (f x)

source

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

source

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

source

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

source

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

source

theorem set.image_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) (a : set α) :

f ∘ g '' a = f '' (g '' a)

source

theorem set.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (s : set α) :

g '' (f '' s) = (λ (x : α), g (f x)) '' s

A variant of image_comp, useful for rewriting

source

theorem set.image_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {β' : Type u_4} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) :

f '' (g '' s) = g' '' (f' '' s)

source

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)

source

theorem function.commute.set_image {α : Type u_1} {f g : α → α} (h : function.commute f g) :

function.commute (set.image f) (set.image g)

source

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

f '' a ⊆ f '' b

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

source

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 ⊆.

source

theorem set.image_union {α : Type u_1} {β : Type u_2} (f : α → β) (s t : set α) :

f '' (s ∪ t) = f '' s ∪ f '' t

source

@[simp]

theorem set.image_empty {α : Type u_1} {β : Type u_2} (f : α → β) :

f '' ∅ = ∅

source

theorem set.image_inter_subset {α : Type u_1} {β : Type u_2} (f : α → β) (s t : set α) :

f '' (s ∩ t) ⊆ f '' s ∩ f '' t

source

theorem set.image_inter_on {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} (h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ s → f x = f y → x = y) :

f '' (s ∩ t) = f '' s ∩ f '' t

source

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

source

theorem set.image_univ_of_surjective {β : Type u_2} {ι : Type u_1} {f : ι → β} (H : function.surjective f) :

f '' set.univ = set.univ

source

@[simp]

theorem set.image_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} :

f '' {a} = {f a}

source

@[simp]

theorem set.nonempty.image_const {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.nonempty) (a : β) :

(λ (_x : α), a) '' s = {a}

source

@[simp]

theorem set.image_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :

f '' s = ∅ ↔ s = ∅

source

theorem set.preimage_compl_eq_image_compl {α : Type u_1} [boolean_algebra α] (S : set α) :

has_compl.compl ⁻¹' S = has_compl.compl '' S

source

theorem set.mem_compl_image {α : Type u_1} [boolean_algebra α] (t : α) (S : set α) :

t ∈ has_compl.compl '' S ↔ tᶜ ∈ S

source

@[simp]

theorem set.image_id' {α : Type u_1} (s : set α) :

(λ (x : α), x) '' s = s

A variant of image_id

source

theorem set.image_id {α : Type u_1} (s : set α) :

id '' s = s

source

theorem set.compl_compl_image {α : Type u_1} [boolean_algebra α] (S : set α) :

has_compl.compl '' (has_compl.compl '' S) = S

source

theorem set.image_insert_eq {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {s : set α} :

f '' has_insert.insert a s = has_insert.insert (f a) (f '' s)

source

theorem set.image_pair {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α) :

f '' {a, b} = {f a, f b}

source

theorem set.image_subset_preimage_of_inverse {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (I : function.left_inverse g f) (s : set α) :

f '' s ⊆ g ⁻¹' s

source

theorem set.preimage_subset_image_of_inverse {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (I : function.left_inverse g f) (s : set β) :

f ⁻¹' s ⊆ g '' s

source

theorem set.image_eq_preimage_of_inverse {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :

set.image f = set.preimage g

source

theorem set.mem_image_iff_of_inverse {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {b : β} {s : set α} (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :

b ∈ f '' s ↔ g b ∈ s

source

theorem set.image_compl_subset {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (H : function.injective f) :

f '' sᶜ ⊆ (f '' s)ᶜ

source

theorem set.subset_image_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (H : function.surjective f) :

(f '' s)ᶜ ⊆ f '' sᶜ

source

theorem set.image_compl_eq {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (H : function.bijective f) :

f '' sᶜ = (f '' s)ᶜ

source

theorem set.subset_image_diff {α : Type u_1} {β : Type u_2} (f : α → β) (s t : set α) :

f '' s \ f '' t ⊆ f '' (s \ t)

source

theorem set.subset_image_symm_diff {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} :

(f '' s) ∆ (f '' t) ⊆ f '' s ∆ t

source

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

source

theorem set.image_symm_diff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (s t : set α) :

f '' s ∆ t = (f '' s) ∆ (f '' t)

source

theorem set.nonempty.image {α : Type u_1} {β : Type u_2} (f : α → β) {s : set α} :

s.nonempty → (f '' s).nonempty

source

theorem set.nonempty.of_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :

(f '' s).nonempty → s.nonempty

source

@[simp]

theorem set.nonempty_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :

(f '' s).nonempty ↔ s.nonempty

source

theorem set.nonempty.preimage {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.nonempty) {f : α → β} (hf : function.surjective f) :

(f ⁻¹' s).nonempty

source

@[protected, instance]

def set.image.nonempty {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) [nonempty ↥s] :

nonempty ↥(f '' s)

source

@[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

source

theorem set.image_preimage_subset {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :

f '' (f ⁻¹' s) ⊆ s

source

theorem set.subset_preimage_image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :

s ⊆ f ⁻¹' (f '' s)

source

theorem set.preimage_image_eq {α : Type u_1} {β : Type u_2} {f : α → β} (s : set α) (h : function.injective f) :

f ⁻¹' (f '' s) = s

source

theorem set.image_preimage_eq {α : Type u_1} {β : Type u_2} {f : α → β} (s : set β) (h : function.surjective f) :

f '' (f ⁻¹' s) = s

source

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

source

theorem set.image_inter_preimage {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (t : set β) :

f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

source

theorem set.image_preimage_inter {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (t : set β) :

f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

source

@[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

source

theorem set.image_diff_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {t : set β} :

f '' (s \ f ⁻¹' t) = f '' s \ t

source

theorem set.compl_image {α : Type u_1} :

set.image has_compl.compl = set.preimage has_compl.compl

source

theorem set.compl_image_set_of {α : Type u_1} {p : set α → Prop} :

has_compl.compl '' {s : set α | p s} = {s : set α | p sᶜ}

source

theorem set.inter_preimage_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) (f : α → β) :

s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)

source

theorem set.union_preimage_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) (f : α → β) :

s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)

source

theorem set.subset_image_union {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (t : set β) :

f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t

source

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

source

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

source

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

source

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.fst, g x.snd) ∈ r} = (λ (a : α × α), (⟦a.fst ⟧, ⟦a.snd ⟧)) '' ((λ (a : α × α), (h a.fst, h a.snd)) ⁻¹' r)

source

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)

source

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

↥s → ↥(f '' s)

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

Equations

set.image_factorization f s = λ (p : ↥s), ⟨f p.val, _⟩

source

theorem set.image_factorization_eq {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :

subtype.val ∘ set.image_factorization f s = f ∘ subtype.val

source

theorem set.surjective_onto_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :

function.surjective (set.image_factorization f s)

source

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.

source

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

𝒫has_insert.insert a s = 𝒫s ∪ has_insert.insert a '' 𝒫s

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

source

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}

Instances for set.range

set.ord_connected_range

Instances for ↥set.range

source

@[simp]

theorem set.mem_range {α : Type u_1} {ι : Sort u_4} {f : ι → α} {x : α} :

x ∈ set.range f ↔ ∃ (y : ι), f y = x

source

@[simp]

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

f i ∈ set.range f

source

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)

source

theorem set.forall_subtype_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : ↥(set.range f) → Prop} :

(∀ (a : ↥(set.range f)), p a) ↔ ∀ (i : ι), p ⟨f i, _⟩

source

theorem set.exists_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop} :

(∃ (a : α) (H : a ∈ set.range f), p a) ↔ ∃ (i : ι), p (f i)

source

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)

source

theorem set.exists_subtype_range_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : ↥(set.range f) → Prop} :

(∃ (a : ↥(set.range f)), p a) ↔ ∃ (i : ι), p ⟨f i, _⟩

source

theorem set.range_iff_surjective {α : Type u_1} {ι : Sort u_4} {f : ι → α} :

set.range f = set.univ ↔ function.surjective f

source

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.

source

@[simp]

theorem set.image_univ {α : Type u_1} {β : Type u_2} {f : α → β} :

f '' set.univ = set.range f

source

theorem set.image_subset_range {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :

f '' s ⊆ set.range f

source

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

source

theorem nat.mem_range_succ (i : ℕ) :

i ∈ set.range nat.succ ↔ 0 < i

source

theorem set.nonempty.preimage' {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.nonempty) {f : α → β} (hf : s ⊆ set.range f) :

(f ⁻¹' s).nonempty

source

theorem set.range_comp {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α) :

set.range (g ∘ f) = g '' set.range f

source

theorem set.range_subset_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : set α} :

set.range f ⊆ s ↔ ∀ (y : ι), f y ∈ s

source

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)

source

theorem set.range_comp_subset_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) :

set.range (g ∘ f) ⊆ set.range g

source

theorem set.range_nonempty_iff_nonempty {α : Type u_1} {ι : Sort u_4} {f : ι → α} :

(set.range f).nonempty ↔ nonempty ι

source

theorem set.range_nonempty {α : Type u_1} {ι : Sort u_4} [h : nonempty ι] (f : ι → α) :

(set.range f).nonempty

source

@[simp]

theorem set.range_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ι → α} :

set.range f = ∅ ↔ is_empty ι

source

theorem set.range_eq_empty {α : Type u_1} {ι : Sort u_4} [is_empty ι] (f : ι → α) :

set.range f = ∅

source

@[protected, instance]

def set.range.nonempty {α : Type u_1} {ι : Sort u_4} [nonempty ι] (f : ι → α) :

nonempty ↥(set.range f)

source

@[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

source

theorem set.insert_image_compl_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :

has_insert.insert (f x) (f '' {x}ᶜ) = set.range f

source

theorem set.image_preimage_eq_inter_range {α : Type u_1} {β : Type u_2} {f : α → β} {t : set β} :

f '' (f ⁻¹' t) = t ∩ set.range f

source

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

source

theorem set.image_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :

f '' (f ⁻¹' s) = s ↔ s ⊆ set.range f

source

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

source

@[simp]

theorem set.exists_subset_range_and_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : set β → Prop} :

(∃ (s : set β), s ⊆ set.range f ∧ p s) ↔ ∃ (s : set α), p (f '' s)

source

theorem set.exists_subset_range_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : set β → Prop} :

(∃ (s : set β) (H : s ⊆ set.range f), p s) ↔ ∃ (s : set α), p (f '' s)

source

theorem set.range_image {α : Type u_1} {β : Type u_2} (f : α → β) :

set.range (set.image f) = 𝒫set.range f

source

theorem set.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {s t : set α} {f : β → α} (hs : s ⊆ set.range f) :

f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

source

theorem set.preimage_eq_preimage' {α : Type u_1} {β : Type u_2} {s t : set α} {f : β → α} (hs : s ⊆ set.range f) (ht : t ⊆ set.range f) :

f ⁻¹' s = f ⁻¹' t ↔ s = t

source

@[simp]

theorem set.preimage_inter_range {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :

f ⁻¹' (s ∩ set.range f) = f ⁻¹' s

source

@[simp]

theorem set.preimage_range_inter {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :

f ⁻¹' (set.range f ∩ s) = f ⁻¹' s

source

theorem set.preimage_image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :

f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s

source

@[simp]

theorem set.range_id {α : Type u_1} :

set.range id = set.univ

source

@[simp]

theorem set.range_id' {α : Type u_1} :

set.range (λ (x : α), x) = set.univ

source

@[simp]

theorem prod.range_fst {α : Type u_1} {β : Type u_2} [nonempty β] :

set.range prod.fst = set.univ

source

@[simp]

theorem prod.range_snd {α : Type u_1} {β : Type u_2} [nonempty α] :

set.range prod.snd = set.univ

source

@[simp]

theorem set.range_eval {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), nonempty (α i)] (i : ι) :

set.range (function.eval i) = set.univ

source

theorem set.range_inl {α : Type u_1} {β : Type u_2} :

set.range sum.inl = {x : α ⊕ β | ↥(x.is_left)}

source

theorem set.range_inr {α : Type u_1} {β : Type u_2} :

set.range sum.inr = {x : α ⊕ β | ↥(x.is_right)}

source

theorem set.is_compl_range_inl_range_inr {α : Type u_1} {β : Type u_2} :

is_compl (set.range sum.inl) (set.range sum.inr)

source

@[simp]

theorem set.range_inl_union_range_inr {α : Type u_1} {β : Type u_2} :

set.range sum.inl ∪ set.range sum.inr = set.univ

source

@[simp]

theorem set.range_inl_inter_range_inr {α : Type u_1} {β : Type u_2} :

set.range sum.inl ∩ set.range sum.inr = ∅

source

@[simp]

theorem set.range_inr_union_range_inl {α : Type u_1} {β : Type u_2} :

set.range sum.inr ∪ set.range sum.inl = set.univ

source

@[simp]

theorem set.range_inr_inter_range_inl {α : Type u_1} {β : Type u_2} :

set.range sum.inr ∩ set.range sum.inl = ∅

source

@[simp]

theorem set.preimage_inl_image_inr {α : Type u_1} {β : Type u_2} (s : set β) :

sum.inl ⁻¹' (sum.inr '' s) = ∅

source

@[simp]

theorem set.preimage_inr_image_inl {α : Type u_1} {β : Type u_2} (s : set α) :

sum.inr ⁻¹' (sum.inl '' s) = ∅

source

@[simp]

theorem set.preimage_inl_range_inr {α : Type u_1} {β : Type u_2} :

sum.inl ⁻¹' set.range sum.inr = ∅

source

@[simp]

theorem set.preimage_inr_range_inl {α : Type u_1} {β : Type u_2} :

sum.inr ⁻¹' set.range sum.inl = ∅

source

@[simp]

theorem set.compl_range_inl {α : Type u_1} {β : Type u_2} :

(set.range sum.inl)ᶜ = set.range sum.inr

source

@[simp]

theorem set.compl_range_inr {α : Type u_1} {β : Type u_2} :

(set.range sum.inr)ᶜ = set.range sum.inl

source

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

source

@[simp]

theorem set.range_quot_mk {α : Type u_1} (r : α → α → Prop) :

set.range (quot.mk r) = set.univ

source

@[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

source

@[simp]

theorem set.range_quotient_mk {α : Type u_1} [setoid α] :

set.range (λ (x : α), ⟦x⟧) = set.univ

source

@[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

source

@[simp]

theorem set.range_quotient_mk' {α : Type u_1} {s : setoid α} :

set.range quotient.mk' = set.univ

source

@[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 (λ (x : quotient s), x.lift_on' f hf) = set.range f

source

@[protected, instance]

def set.can_lift {α : Type u_1} {β : Type u_2} (c : out_param (β → α)) (p : out_param (α → Prop)) [can_lift α β c p] :

can_lift (set α) (set β) (set.image c) (λ (s : set α), ∀ (x : α), x ∈ s → p x)

Equations

set.can_lift c p = {prf := _}

source

theorem set.range_const_subset {α : Type u_1} {ι : Sort u_4} {c : α} :

set.range (λ (x : ι), c) ⊆ {c}

source

@[simp]

theorem set.range_const {α : Type u_1} {ι : Sort u_4} [nonempty ι] {c : α} :

set.range (λ (x : ι), c) = {c}

source

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) = coe ⁻¹' (f '' {x : α | p x})

source

theorem set.image_swap_eq_preimage_swap {α : Type u_1} {β : Type u_2} :

set.image prod.swap = set.preimage prod.swap

source

theorem set.preimage_singleton_nonempty {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} :

(f ⁻¹' {y}).nonempty ↔ y ∈ set.range f

source

theorem set.preimage_singleton_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} :

f ⁻¹' {y} = ∅ ↔ y ∉ set.range f

source

theorem set.range_subset_singleton {α : Type u_1} {ι : Sort u_4} {f : ι → α} {x : α} :

set.range f ⊆ {x} ↔ f = function.const ι x

source

theorem set.image_compl_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : set β} :

f '' (f ⁻¹' s)ᶜ = set.range f \ s

source

def set.range_factorization {β : Type u_2} {ι : Sort u_4} (f : ι → β) :

ι → ↥(set.range f)

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

Equations

set.range_factorization f = λ (i : ι), ⟨f i, _⟩

source

theorem set.range_factorization_eq {β : Type u_2} {ι : Sort u_4} {f : ι → β} :

subtype.val ∘ set.range_factorization f = f

source

@[simp]

theorem set.range_factorization_coe {β : Type u_2} {ι : Sort u_4} (f : ι → β) (a : ι) :

↑(set.range_factorization f a) = f a

source

@[simp]

theorem set.coe_comp_range_factorization {β : Type u_2} {ι : Sort u_4} (f : ι → β) :

coe ∘ set.range_factorization f = f

source

theorem set.surjective_onto_range {α : Type u_1} {ι : Sort u_4} {f : ι → α} :

function.surjective (set.range_factorization f)

source

theorem set.image_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :

f '' s = set.range (λ (x : ↥s), f ↑x)

source

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)

source

@[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

source

theorem set.range_ite_subset' {α : Type u_1} {β : Type u_2} {p : Prop} [decidable p] {f g : α → β} :

set.range (ite p f g) ⊆ set.range f ∪ set.range g

source

theorem set.range_ite_subset {α : Type u_1} {β : Type u_2} {p : α → Prop} [decidable_pred p] {f g : α → β} :

set.range (λ (x : α), ite (p x) (f x) (g x)) ⊆ set.range f ∪ set.range g

source

@[simp]

theorem set.preimage_range {α : Type u_1} {β : Type u_2} (f : α → β) :

f ⁻¹' set.range f = set.univ

source

theorem set.range_unique {α : Type u_1} {ι : Sort u_4} {f : ι → α} [h : unique ι] :

set.range f = {f inhabited.default}

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

source

theorem set.range_diff_image_subset {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :

set.range f \ f '' s ⊆ f '' sᶜ

source

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ᶜ

source

@[simp]

theorem set.range_inclusion {α : Type u_1} {s t : set α} (h : s ⊆ t) :

set.range (set.inclusion h) = {x : ↥t | ↑x ∈ s}

source

@[irreducible]

noncomputable def set.range_splitting {α : 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.range_splitting f = λ (x : ↥(set.range f)), Exists.some _

source

theorem set.apply_range_splitting {α : Type u_1} {β : Type u_2} (f : α → β) (x : ↥(set.range f)) :

f (set.range_splitting f x) = ↑x

source

@[simp]

theorem set.comp_range_splitting {α : Type u_1} {β : Type u_2} (f : α → β) :

f ∘ set.range_splitting f = coe

source

theorem set.left_inverse_range_splitting {α : Type u_1} {β : Type u_2} (f : α → β) :

function.left_inverse (set.range_factorization f) (set.range_splitting f)

source

theorem set.range_splitting_injective {α : Type u_1} {β : Type u_2} (f : α → β) :

function.injective (set.range_splitting f)

source

theorem set.right_inverse_range_splitting {α : Type u_1} {β : Type u_2} {f : α → β} (h : function.injective f) :

function.right_inverse (set.range_factorization f) (set.range_splitting f)

source

theorem set.preimage_range_splitting {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) :

set.preimage (set.range_splitting f) = set.image (set.range_factorization f)

source

theorem set.is_compl_range_some_none (α : Type u_1) :

is_compl (set.range option.some) {option.none}

source

@[simp]

theorem set.compl_range_some (α : Type u_1) :

(set.range option.some)ᶜ = {option.none}

source

@[simp]

theorem set.range_some_inter_none (α : Type u_1) :

set.range option.some ∩ {option.none} = ∅

source

@[simp]

theorem set.range_some_union_none (α : Type u_1) :

set.range option.some ∪ {option.none} = set.univ

source

@[simp]

theorem set.insert_none_range_some (α : Type u_1) :

has_insert.insert option.none (set.range option.some) = set.univ

source

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.

source

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

(f ⁻¹' s).subsingleton

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

source

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.

source

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 an surjective map is a subsingleton, the set is a subsingleton.

source

theorem set.subsingleton_range {β : Type u_2} {α : Sort u_1} [subsingleton α] (f : α → β) :

(set.range f).subsingleton

source

theorem set.nontrivial.preimage {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.nontrivial) {f : α → β} (hf : function.surjective f) :

(f ⁻¹' s).nontrivial

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

source

theorem set.nontrivial.image {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.nontrivial) {f : α → β} (hf : function.injective f) :

(f '' s).nontrivial

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

source

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.

source

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.

source

theorem function.surjective.preimage_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) :

function.injective (set.preimage f)

source

theorem function.injective.preimage_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (s : set α) :

f ⁻¹' (f '' s) = s

source

theorem function.injective.preimage_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) :

function.surjective (set.preimage f)

source

theorem function.injective.subsingleton_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {s : set α} :

(f '' s).subsingleton ↔ s.subsingleton

source

theorem function.surjective.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) (s : set β) :

f '' (f ⁻¹' s) = s

source

theorem function.surjective.image_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) :

function.surjective (set.image f)

source

theorem function.surjective.nonempty_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) {s : set β} :

(f ⁻¹' s).nonempty ↔ s.nonempty

source

theorem function.injective.image_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) :

function.injective (set.image f)

source

theorem function.surjective.preimage_subset_preimage_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set β} (hf : function.surjective f) :

f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

source

theorem function.surjective.range_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {f : ι → ι'} (hf : function.surjective f) (g : ι' → α) :

set.range (g ∘ f) = set.range g

source

theorem function.injective.mem_range_iff_exists_unique {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {b : β} :

b ∈ set.range f ↔ ∃! (a : α), f a = b

source

theorem function.injective.exists_unique_of_mem_range {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {b : β} (hb : b ∈ set.range f) :

∃! (a : α), f a = b

source

theorem function.injective.compl_image_eq {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (s : set α) :

(f '' s)ᶜ = f '' sᶜ ∪ (set.range f)ᶜ

source

theorem function.left_inverse.image_image {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : function.left_inverse g f) (s : set α) :

g '' (f '' s) = s

source

theorem function.left_inverse.preimage_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (h : function.left_inverse g f) (s : set α) :

f ⁻¹' (g ⁻¹' s) = s

source

@[protected]

theorem function.involutive.preimage {α : Type u_1} {f : α → α} (hf : function.involutive f) :

function.involutive (set.preimage f)

source

@[simp]

theorem equiv_like.range_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {E : Type u_6} [equiv_like E ι ι'] (f : ι' → α) (e : E) :

set.range (f ∘ ⇑e) = set.range f

source

theorem subtype.coe_image {α : Type u_1} {p : α → Prop} {s : set (subtype p)} :

coe '' s = {x : α | ∃ (h : p x), ⟨x, h⟩ ∈ s}

source

@[simp]

theorem subtype.coe_image_of_subset {α : Type u_1} {s t : set α} (h : t ⊆ s) :

coe '' {x : ↥s | ↑x ∈ t} = t

source

theorem subtype.range_coe {α : Type u_1} {s : set α} :

set.range coe = s

source

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.

source

@[simp]

theorem subtype.range_coe_subtype {α : Type u_1} {p : α → Prop} :

set.range coe = {x : α | p x}

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

source

@[simp]

theorem subtype.coe_preimage_self {α : Type u_1} (s : set α) :

coe ⁻¹' s = set.univ

source

theorem subtype.range_val_subtype {α : Type u_1} {p : α → Prop} :

set.range subtype.val = {x : α | p x}

source

theorem subtype.coe_image_subset {α : Type u_1} (s : set α) (t : set ↥s) :

coe '' t ⊆ s

source

theorem subtype.coe_image_univ {α : Type u_1} (s : set α) :

coe '' set.univ = s

source

@[simp]

theorem subtype.image_preimage_coe {α : Type u_1} (s t : set α) :

coe '' (coe ⁻¹' t) = t ∩ s

source

theorem subtype.image_preimage_val {α : Type u_1} (s t : set α) :

subtype.val '' (subtype.val ⁻¹' t) = t ∩ s

source

theorem subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s t u : set α} :

coe ⁻¹' t = coe ⁻¹' u ↔ t ∩ s = u ∩ s

source

@[simp]

theorem subtype.preimage_coe_inter_self {α : Type u_1} (s t : set α) :

coe ⁻¹' (t ∩ s) = coe ⁻¹' t

source

theorem subtype.preimage_val_eq_preimage_val_iff {α : Type u_1} (s t u : set α) :

subtype.val ⁻¹' t = subtype.val ⁻¹' u ↔ t ∩ s = u ∩ s

source

theorem subtype.exists_set_subtype {α : Type u_1} {t : set α} (p : set α → Prop) :

(∃ (s : set ↥t), p (coe '' s)) ↔ ∃ (s : set α), s ⊆ t ∧ p s

source

theorem subtype.preimage_coe_nonempty {α : Type u_1} {s t : set α} :

(coe ⁻¹' t).nonempty ↔ (s ∩ t).nonempty

source

theorem subtype.preimage_coe_eq_empty {α : Type u_1} {s t : set α} :

coe ⁻¹' t = ∅ ↔ s ∩ t = ∅

source

@[simp]

theorem subtype.preimage_coe_compl {α : Type u_1} (s : set α) :

coe ⁻¹' sᶜ = ∅

source

@[simp]

theorem subtype.preimage_coe_compl' {α : Type u_1} (s : set α) :

coe ⁻¹' s = ∅

source

theorem option.injective_iff {α : Type u_1} {β : Type u_2} {f : option α → β} :

function.injective f ↔ function.injective (f ∘ option.some) ∧ f option.none ∉ set.range (f ∘ option.some)

source

theorem option.range_eq {α : Type u_1} {β : Type u_2} (f : option α → β) :

set.range f = has_insert.insert (f option.none) (set.range (f ∘ option.some))

source

theorem with_bot.range_eq {α : Type u_1} {β : Type u_2} (f : with_bot α → β) :

set.range f = has_insert.insert (f ⊥) (set.range (f ∘ coe))

source

theorem with_top.range_eq {α : Type u_1} {β : Type u_2} (f : with_top α → β) :

set.range f = has_insert.insert (f ⊤) (set.range (f ∘ coe))

source

@[simp]

theorem set.preimage_injective {α : Type u_1} {β : Type u_2} {f : α → β} :

function.injective (set.preimage f) ↔ function.surjective f

source

@[simp]

theorem set.preimage_surjective {α : Type u_1} {β : Type u_2} {f : α → β} :

function.surjective (set.preimage f) ↔ function.injective f

source

@[simp]

theorem set.image_surjective {α : Type u_1} {β : Type u_2} {f : α → β} :

function.surjective (set.image f) ↔ function.surjective f

source

@[simp]

theorem set.image_injective {α : Type u_1} {β : Type u_2} {f : α → β} :

function.injective (set.image f) ↔ function.injective f

source

theorem set.preimage_eq_iff_eq_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.bijective f) {s : set β} {t : set α} :

f ⁻¹' s = t ↔ s = f '' t

source

theorem set.eq_preimage_iff_image_eq {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.bijective f) {s : set α} {t : set β} :

s = f ⁻¹' t ↔ f '' s = t

source

theorem disjoint.preimage {α : Type u_1} {β : Type u_2} (f : α → β) {s t : set β} (h : disjoint s t) :

disjoint (f ⁻¹' s) (f ⁻¹' t)

source

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)

source

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)

source

theorem disjoint.of_image {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} (h : disjoint (f '' s) (f '' t)) :

disjoint s t

source

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

source

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

source