mathlib documentation

data.set.function

Functions over sets

Main definitions

Predicate

Functions

Restrict

source
def set.restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) (a : ↥s) :
β

Restrict domain of a function f to a set s. Same as subtype.restrict but this version takes an argument ↥s instead of subtype s.

Equations
source
theorem set.restrict_eq {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.restrict f s = f ∘ coe

source
@[simp]
theorem set.restrict_apply {α : Type u} {β : Type v} (f : α → β) (s : set α) (x : ↥s) :
set.restrict f s x = f ↑x

source
@[simp]
theorem set.range_restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.range (set.restrict f s) = f '' s

source
def set.cod_restrict {α : Type u} {β : Type v} (f : α → β) (s : set β) (h : ∀ (x : α), f x ∈ s) (a : α) :
↥s

Restrict codomain of a function f to a set s. Same as subtype.coind but this version has codomain ↥s instead of subtype s.

Equations
source
@[simp]
theorem set.coe_cod_restrict_apply {α : Type u} {β : Type v} (f : α → β) (s : set β) (h : ∀ (x : α), f x ∈ s) (x : α) :
↑(set.cod_restrict f s h x) = f x

Equality on a set

source
def set.eq_on {α : Type u} {β : Type v} (f₁ f₂ : α → β) (s : set α) :
Prop

Two functions f₁ f₂ : α → β are equal on s if f₁ x = f₂ x for all x ∈ a.

Equations
  • set.eq_on f₁ f₂ s = ∀ ⦃x : α⦄, x ∈ s → f₁ x = f₂ x
source
theorem set.eq_on.symm {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (h : set.eq_on f₁ f₂ s) :
set.eq_on f₂ f₁ s

source
theorem set.eq_on_comm {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} :
set.eq_on f₁ f₂ s ↔ set.eq_on f₂ f₁ s

source
theorem set.eq_on_refl {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.eq_on f f s

source
theorem set.eq_on.trans {α : Type u} {β : Type v} {s : set α} {f₁ f₂ f₃ : α → β} (h₁ : set.eq_on f₁ f₂ s) (h₂ : set.eq_on f₂ f₃ s) :
set.eq_on f₁ f₃ s

source
theorem set.eq_on.image_eq {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (heq : set.eq_on f₁ f₂ s) :
f₁ '' s = f₂ '' s

source
theorem set.eq_on.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {f₁ f₂ : α → β} (hs : s₁ ⊆ s₂) (hf : set.eq_on f₁ f₂ s₂) :
set.eq_on f₁ f₂ s₁

source
theorem set.comp_eq_of_eq_on_range {α : Type u} {β : Type v} {ι : Sort u_1} {f : ι → α} {g₁ g₂ : α → β} (h : set.eq_on g₁ g₂ (set.range f)) :
g₁ ∘ f = g₂ ∘ f

maps to

source
def set.maps_to {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
Prop

maps_to f a b means that the image of a is contained in b.

Equations
source
def set.maps_to.restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) (h : set.maps_to f s t) (a : ↥s) :
↥t

Given a map f sending s : set α into t : set β, restrict domain of f to s and the codomain to t. Same as subtype.map.

Equations
source
@[simp]
theorem set.maps_to.coe_restrict_apply {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.maps_to f s t) (x : ↥s) :
↑(set.maps_to.restrict f s t h x) = f ↑x

source
theorem set.maps_to' {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
set.maps_to f s t ↔ f '' s ⊆ t

source
theorem set.maps_to_empty {α : Type u} {β : Type v} (f : α → β) (t : set β) :
set.maps_to f ∅ t

source
theorem set.maps_to.image_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.maps_to f s t) :
f '' s ⊆ t

source
theorem set.maps_to.congr {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h₁ : set.maps_to f₁ s t) (h : set.eq_on f₁ f₂ s) :
set.maps_to f₂ s t

source
theorem set.eq_on.maps_to_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (H : set.eq_on f₁ f₂ s) :
set.maps_to f₁ s t ↔ set.maps_to f₂ s t

source
theorem set.maps_to.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {p : set γ} {f : α → β} {g : β → γ} (h₁ : set.maps_to g t p) (h₂ : set.maps_to f s t) :
set.maps_to (g ∘ f) s p

source
theorem set.maps_to.iterate {α : Type u} {f : α → α} {s : set α} (h : set.maps_to f s s) (n : ℕ) :
set.maps_to f^[n] s s

source
theorem set.maps_to.iterate_restrict {α : Type u} {f : α → α} {s : set α} (h : set.maps_to f s s) (n : ℕ) :
set.maps_to.restrict f s s h^[n] = set.maps_to.restrict f^[n] s s _

source
theorem set.maps_to.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (hs : s₂ ⊆ s₁) (ht : t₁ ⊆ t₂) (hf : set.maps_to f s₁ t₁) :
set.maps_to f s₂ t₂

source
theorem set.maps_to.union_union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.maps_to f s₁ t₁) (h₂ : set.maps_to f s₂ t₂) :
set.maps_to f (s₁ ∪ s₂) (t₁ ∪ t₂)

source
theorem set.maps_to.union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t : set β} {f : α → β} (h₁ : set.maps_to f s₁ t) (h₂ : set.maps_to f s₂ t) :
set.maps_to f (s₁ ∪ s₂) t

source
theorem set.maps_to.inter {α : Type u} {β : Type v} {s : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.maps_to f s t₁) (h₂ : set.maps_to f s t₂) :
set.maps_to f s (t₁ ∩ t₂)

source
theorem set.maps_to.inter_inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.maps_to f s₁ t₁) (h₂ : set.maps_to f s₂ t₂) :
set.maps_to f (s₁ ∩ s₂) (t₁ ∩ t₂)

source
theorem set.maps_to_univ {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.maps_to f s set.univ

source
theorem set.maps_to_image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.maps_to f s (f '' s)

source
theorem set.maps_to_preimage {α : Type u} {β : Type v} (f : α → β) (t : set β) :
set.maps_to f (f ⁻¹' t) t

source
theorem set.maps_to_range {α : Type u} (f s : set α) :
set.maps_to f s (set.range f)

Injectivity on a set

source
def set.inj_on {α : Type u} {β : Type v} (f : α → β) (s : set α) :
Prop

f is injective on a if the restriction of f to a is injective.

Equations
  • set.inj_on f s = ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂
source
theorem set.inj_on_empty {α : Type u} {β : Type v} (f : α → β) :
set.inj_on f ∅

source
theorem set.inj_on.congr {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (h₁ : set.inj_on f₁ s) (h : set.eq_on f₁ f₂ s) :
set.inj_on f₂ s

source
theorem set.eq_on.inj_on_iff {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (H : set.eq_on f₁ f₂ s) :
set.inj_on f₁ s ↔ set.inj_on f₂ s

source
theorem set.inj_on.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {f : α → β} (h : s₁ ⊆ s₂) (ht : set.inj_on f s₂) :
set.inj_on f s₁

source
theorem set.inj_on_insert {α : Type u} {β : Type v} {f : α → β} {s : set α} {a : α} (has : a ∉ s) :
set.inj_on f (insert a s) ↔ set.inj_on f s ∧ f a ∉ f '' s

source
theorem set.injective_iff_inj_on_univ {α : Type u} {β : Type v} {f : α → β} :
function.injective f ↔ set.inj_on f set.univ

source
theorem set.inj_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f : α → β} {g : β → γ} (hg : set.inj_on g t) (hf : set.inj_on f s) (h : set.maps_to f s t) :
set.inj_on (g ∘ f) s

source
theorem set.inj_on_iff_injective {α : Type u} {β : Type v} {s : set α} {f : α → β} :
set.inj_on f s ↔ function.injective (set.restrict f s)

source
theorem set.inj_on.inv_fun_on_image {α : Type u} {β : Type v} {s₁ s₂ : set α} {f : α → β} [nonempty α] (h : set.inj_on f s₂) (ht : s₁ ⊆ s₂) :
function.inv_fun_on f s₂ '' (f '' s₁) = s₁

source
theorem set.inj_on_preimage {α : Type u} {β : Type v} {f : α → β} {B : set (set β)} (hB : B ⊆ 𝒫set.range f) :
set.inj_on (set.preimage f) B

Surjectivity on a set

source
def set.surj_on {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
Prop

f is surjective from a to b if b is contained in the image of a.

Equations
source
theorem set.surj_on.subset_range {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.surj_on f s t) :
t ⊆ set.range f

source
theorem set.surj_on_empty {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set.surj_on f s ∅

source
theorem set.surj_on.comap_nonempty {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.surj_on f s t) (ht : t.nonempty) :
s.nonempty

source
theorem set.surj_on.congr {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h : set.surj_on f₁ s t) (H : set.eq_on f₁ f₂ s) :
set.surj_on f₂ s t

source
theorem set.eq_on.surj_on_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h : set.eq_on f₁ f₂ s) :
set.surj_on f₁ s t ↔ set.surj_on f₂ s t

source
theorem set.surj_on.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (hf : set.surj_on f s₁ t₂) :
set.surj_on f s₂ t₁

source
theorem set.surj_on.union {α : Type u} {β : Type v} {s : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.surj_on f s t₁) (h₂ : set.surj_on f s t₂) :
set.surj_on f s (t₁ ∪ t₂)

source
theorem set.surj_on.union_union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.surj_on f s₁ t₁) (h₂ : set.surj_on f s₂ t₂) :
set.surj_on f (s₁ ∪ s₂) (t₁ ∪ t₂)

source
theorem set.surj_on.inter_inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.surj_on f s₁ t₁) (h₂ : set.surj_on f s₂ t₂) (h : set.inj_on f (s₁ ∪ s₂)) :
set.surj_on f (s₁ ∩ s₂) (t₁ ∩ t₂)

source
theorem set.surj_on.inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t : set β} {f : α → β} (h₁ : set.surj_on f s₁ t) (h₂ : set.surj_on f s₂ t) (h : set.inj_on f (s₁ ∪ s₂)) :
set.surj_on f (s₁ ∩ s₂) t

source
theorem set.surj_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {p : set γ} {f : α → β} {g : β → γ} (hg : set.surj_on g t p) (hf : set.surj_on f s t) :
set.surj_on (g ∘ f) s p

source
theorem set.surjective_iff_surj_on_univ {α : Type u} {β : Type v} {f : α → β} :
function.surjective f ↔ set.surj_on f set.univ set.univ

source
theorem set.surj_on_iff_surjective {α : Type u} {β : Type v} {s : set α} {f : α → β} :
set.surj_on f s set.univ ↔ function.surjective (set.restrict f s)

source
theorem set.surj_on.image_eq_of_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h₁ : set.surj_on f s t) (h₂ : set.maps_to f s t) :
f '' s = t

Bijectivity

source
def set.bij_on {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
Prop

f is bijective from s to t if f is injective on s and f '' s = t.

Equations
source
theorem set.bij_on.maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.bij_on f s t) :
set.maps_to f s t

source
theorem set.bij_on.inj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.bij_on f s t) :
set.inj_on f s

source
theorem set.bij_on.surj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.bij_on f s t) :
set.surj_on f s t

source
theorem set.bij_on.mk {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h₁ : set.maps_to f s t) (h₂ : set.inj_on f s) (h₃ : set.surj_on f s t) :
set.bij_on f s t

source
theorem set.bij_on_empty {α : Type u} {β : Type v} (f : α → β) :
set.bij_on f ∅ ∅

source
theorem set.bij_on.inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.bij_on f s₁ t₁) (h₂ : set.bij_on f s₂ t₂) (h : set.inj_on f (s₁ ∪ s₂)) :
set.bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂)

source
theorem set.bij_on.union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : set.bij_on f s₁ t₁) (h₂ : set.bij_on f s₂ t₂) (h : set.inj_on f (s₁ ∪ s₂)) :
set.bij_on f (s₁ ∪ s₂) (t₁ ∪ t₂)

source
theorem set.bij_on.subset_range {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.bij_on f s t) :
t ⊆ set.range f

source
theorem set.inj_on.bij_on_image {α : Type u} {β : Type v} {s : set α} {f : α → β} (h : set.inj_on f s) :
set.bij_on f s (f '' s)

source
theorem set.bij_on.congr {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h₁ : set.bij_on f₁ s t) (h : set.eq_on f₁ f₂ s) :
set.bij_on f₂ s t

source
theorem set.eq_on.bij_on_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (H : set.eq_on f₁ f₂ s) :
set.bij_on f₁ s t ↔ set.bij_on f₂ s t

source
theorem set.bij_on.image_eq {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : set.bij_on f s t) :
f '' s = t

source
theorem set.bij_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {p : set γ} {f : α → β} {g : β → γ} (hg : set.bij_on g t p) (hf : set.bij_on f s t) :
set.bij_on (g ∘ f) s p

source
theorem set.bijective_iff_bij_on_univ {α : Type u} {β : Type v} {f : α → β} :
function.bijective f ↔ set.bij_on f set.univ set.univ

left inverse

source
def set.left_inv_on {α : Type u} {β : Type v} (f' : β → α) (f : α → β) (s : set α) :
Prop

g is a left inverse to f on a means that g (f x) = x for all x ∈ a.

Equations
source
theorem set.left_inv_on.eq_on {α : Type u} {β : Type v} {s : set α} {f : α → β} {f' : β → α} (h : set.left_inv_on f' f s) :
set.eq_on (f' ∘ f) id s

source
theorem set.left_inv_on.eq {α : Type u} {β : Type v} {s : set α} {f : α → β} {f' : β → α} (h : set.left_inv_on f' f s) {x : α} (hx : x ∈ s) :
f' (f x) = x

source
theorem set.left_inv_on.congr_left {α : Type u} {β : Type v} {s : set α} {f : α → β} {f₁' f₂' : β → α} (h₁ : set.left_inv_on f₁' f s) {t : set β} (h₁' : set.maps_to f s t) (heq : set.eq_on f₁' f₂' t) :
set.left_inv_on f₂' f s

source
theorem set.left_inv_on.congr_right {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} {f₁' : β → α} (h₁ : set.left_inv_on f₁' f₁ s) (heq : set.eq_on f₁ f₂ s) :
set.left_inv_on f₁' f₂ s

source
theorem set.left_inv_on.inj_on {α : Type u} {β : Type v} {s : set α} {f : α → β} {f₁' : β → α} (h : set.left_inv_on f₁' f s) :
set.inj_on f s

source
theorem set.left_inv_on.surj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f₁' : β → α} (h : set.left_inv_on f₁' f s) (hf : set.maps_to f s t) :
set.surj_on f₁' t s

source
theorem set.left_inv_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf' : set.left_inv_on f' f s) (hg' : set.left_inv_on g' g t) (hf : set.maps_to f s t) :
set.left_inv_on (f' ∘ g') (g ∘ f) s

Right inverse

source
def set.right_inv_on {α : Type u} {β : Type v} (f' : β → α) (f : α → β) (t : set β) :
Prop

g is a right inverse to f on b if f (g x) = x for all x ∈ b.

Equations
source
theorem set.right_inv_on.eq_on {α : Type u} {β : Type v} {t : set β} {f : α → β} {f' : β → α} (h : set.right_inv_on f' f t) :
set.eq_on (f ∘ f') id t

source
theorem set.right_inv_on.eq {α : Type u} {β : Type v} {t : set β} {f : α → β} {f' : β → α} (h : set.right_inv_on f' f t) {y : β} (hy : y ∈ t) :
f (f' y) = y

source
theorem set.right_inv_on.congr_left {α : Type u} {β : Type v} {t : set β} {f : α → β} {f₁' f₂' : β → α} (h₁ : set.right_inv_on f₁' f t) (heq : set.eq_on f₁' f₂' t) :
set.right_inv_on f₂' f t

source
theorem set.right_inv_on.congr_right {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} {f' : β → α} (h₁ : set.right_inv_on f' f₁ t) (hg : set.maps_to f' t s) (heq : set.eq_on f₁ f₂ s) :
set.right_inv_on f' f₂ t

source
theorem set.right_inv_on.surj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (hf : set.right_inv_on f' f t) (hf' : set.maps_to f' t s) :
set.surj_on f s t

source
theorem set.right_inv_on.comp {α : Type u} {β : Type v} {γ : Type w} {t : set β} {p : set γ} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf : set.right_inv_on f' f t) (hg : set.right_inv_on g' g p) (g'pt : set.maps_to g' p t) :
set.right_inv_on (f' ∘ g') (g ∘ f) p

source
theorem set.inj_on.right_inv_on_of_left_inv_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (hf : set.inj_on f s) (hf' : set.left_inv_on f f' t) (h₁ : set.maps_to f s t) (h₂ : set.maps_to f' t s) :
set.right_inv_on f f' s

source
theorem set.eq_on_of_left_inv_on_of_right_inv_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f₁' f₂' : β → α} (h₁ : set.left_inv_on f₁' f s) (h₂ : set.right_inv_on f₂' f t) (h : set.maps_to f₂' t s) :
set.eq_on f₁' f₂' t

source
theorem set.surj_on.left_inv_on_of_right_inv_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (hf : set.surj_on f s t) (hf' : set.right_inv_on f f' s) :
set.left_inv_on f f' t

Two-side inverses

source
def set.inv_on {α : Type u} {β : Type v} (g : β → α) (f : α → β) (s : set α) (t : set β) :
Prop

g is an inverse to f viewed as a map from a to b

Equations
source
theorem set.inv_on.symm {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : set.inv_on f' f s t) :
set.inv_on f f' t s

source
theorem set.inv_on.bij_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : set.inv_on f' f s t) (hf : set.maps_to f s t) (hf' : set.maps_to f' t s) :
set.bij_on f s t

inv_fun_on is a left/right inverse

source
theorem set.inj_on.left_inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {f : α → β} [nonempty α] (h : set.inj_on f s) :
set.left_inv_on (function.inv_fun_on f s) f s

source
theorem set.surj_on.right_inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : set.surj_on f s t) :
set.right_inv_on (function.inv_fun_on f s) f t

source
theorem set.bij_on.inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : set.bij_on f s t) :
set.inv_on (function.inv_fun_on f s) f s t

source
theorem set.surj_on.inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : set.surj_on f s t) :
set.inv_on (function.inv_fun_on f s) f (function.inv_fun_on f s '' t) t

source
theorem set.surj_on.maps_to_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : set.surj_on f s t) :
set.maps_to (function.inv_fun_on f s) t s

source
theorem set.surj_on.bij_on_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : set.surj_on f s t) :
set.bij_on f (function.inv_fun_on f s '' t) t

source
theorem set.surj_on_iff_exists_bij_on_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
set.surj_on f s t ↔ ∃ (s' : set α) (H : s' ⊆ s), set.bij_on f s' t

Piecewise defined function

source
@[simp]
theorem set.piecewise_empty {α : Type u} {δ : α → Sort y} (f g : Π (i : α), δ i) [Π (i : α), decidable (i ∈ ∅)] :
∅.piecewise f g = g

source
@[simp]
theorem set.piecewise_univ {α : Type u} {δ : α → Sort y} (f g : Π (i : α), δ i) [Π (i : α), decidable (i ∈ set.univ)] :
set.univ.piecewise f g = f

source
@[simp]
theorem set.piecewise_insert_self {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) {j : α} [Π (i : α), decidable (i ∈ insert j s)] :
(insert j s).piecewise f g j = f j

source
@[instance]
def set.compl.decidable_mem {α : Type u} (s : set α) [Π (j : α), decidable (j ∈ s)] (j : α) :
decidable (j ∈ sᶜ)

Equations
source
theorem set.piecewise_insert {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [decidable_eq α] (j : α) [Π (i : α), decidable (i ∈ insert j s)] :
(insert j s).piecewise f g = function.update (s.piecewise f g) j (f j)

source
@[simp]
theorem set.piecewise_eq_of_mem {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] {i : α} (hi : i ∈ s) :
s.piecewise f g i = f i

source
@[simp]
theorem set.piecewise_eq_of_not_mem {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] {i : α} (hi : i ∉ s) :
s.piecewise f g i = g i

source
theorem set.piecewise_eq_on {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j ∈ s)] (f g : α → β) :
set.eq_on (s.piecewise f g) f s

source
theorem set.piecewise_eq_on_compl {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j ∈ s)] (f g : α → β) :
set.eq_on (s.piecewise f g) g sᶜ

source
@[simp]
theorem set.piecewise_insert_of_ne {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] {i j : α} (h : i ≠ j) [Π (i : α), decidable (i ∈ insert j s)] :
(insert j s).piecewise f g i = s.piecewise f g i

source
@[simp]
theorem set.piecewise_compl {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] [Π (i : α), decidable (i ∈ sᶜ)] :
sᶜ.piecewise f g = s.piecewise g f

source
@[simp]
theorem set.piecewise_range_comp {α : Type u} {β : Type v} {ι : Sort u_1} (f : ι → α) [Π (j : α), decidable (j ∈ set.range f)] (g₁ g₂ : α → β) :
(set.range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f

source
theorem set.piecewise_preimage {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j ∈ s)] (f g : α → β) (t : set β) :
s.piecewise f g ⁻¹' t = s ∩ f ⁻¹' t ∪ sᶜ ∩ g ⁻¹' t

source
theorem set.comp_piecewise {α : Type u} {β : Type v} {γ : Type w} (s : set α) [Π (j : α), decidable (j ∈ s)] (h : β → γ) {f g : α → β} {x : α} :
h (s.piecewise f g x) = s.piecewise (h ∘ f) (h ∘ g) x

source
@[simp]
theorem set.piecewise_same {α : Type u} {δ : α → Sort y} (s : set α) (f : Π (i : α), δ i) [Π (j : α), decidable (j ∈ s)] :
s.piecewise f f = f

source
theorem set.range_piecewise {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j ∈ s)] (f g : α → β) :
set.range (s.piecewise f g) = f '' s ∪ g '' sᶜ

source
theorem function.injective.inj_on {α : Type u} {β : Type v} {f : α → β} (h : function.injective f) (s : set α) :
set.inj_on f s

source
theorem function.injective.comp_inj_on {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {s : set α} (hg : function.injective g) (hf : set.inj_on f s) :
set.inj_on (g ∘ f) s

source
theorem function.surjective.surj_on {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) (s : set β) :
set.surj_on f set.univ s

source
theorem function.semiconj.maps_to_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s t : set α} (h : function.semiconj f fa fb) (ha : set.maps_to fa s t) :
set.maps_to fb (f '' s) (f '' t)

source
theorem function.semiconj.maps_to_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : function.semiconj f fa fb) :
set.maps_to fb (set.range f) (set.range f)

source
theorem function.semiconj.surj_on_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s t : set α} (h : function.semiconj f fa fb) (ha : set.surj_on fa s t) :
set.surj_on fb (f '' s) (f '' t)

source
theorem function.semiconj.surj_on_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : function.semiconj f fa fb) (ha : function.surjective fa) :
set.surj_on fb (set.range f) (set.range f)

source
theorem function.semiconj.inj_on_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s : set α} (h : function.semiconj f fa fb) (ha : set.inj_on fa s) (hf : set.inj_on f (fa '' s)) :
set.inj_on fb (f '' s)

source
theorem function.semiconj.inj_on_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : function.semiconj f fa fb) (ha : function.injective fa) (hf : set.inj_on f (set.range fa)) :
set.inj_on fb (set.range f)

source
theorem function.semiconj.bij_on_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s t : set α} (h : function.semiconj f fa fb) (ha : set.bij_on fa s t) (hf : set.inj_on f t) :
set.bij_on fb (f '' s) (f '' t)

source
theorem function.semiconj.bij_on_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : function.semiconj f fa fb) (ha : function.bijective fa) (hf : function.injective f) :
set.bij_on fb (set.range f) (set.range f)

source
theorem function.semiconj.maps_to_preimage {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : function.semiconj f fa fb) {s t : set β} (hb : set.maps_to fb s t) :
set.maps_to fa (f ⁻¹' s) (f ⁻¹' t)

source
theorem function.semiconj.inj_on_preimage {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : function.semiconj f fa fb) {s : set β} (hb : set.inj_on fb s) (hf : set.inj_on f (f ⁻¹' s)) :
set.inj_on fa (f ⁻¹' s)

source
theorem function.update_comp_eq_of_not_mem_range {α : Type u} {β : Type v} {γ : Type w} [decidable_eq β] (g : β → γ) {f : α → β} {i : β} (a : γ) (h : i ∉ set.range f) :
function.update g i a ∘ f = g ∘ f

source
theorem function.update_comp_eq_of_injective {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β] (g : β → γ) {f : α → β} (hf : function.injective f) (i : α) (a : γ) :
function.update g (f i) a ∘ f = function.update (g ∘ f) i a