mathlibdocumentation

data.set.function

Functions over sets #

Main definitions #

Predicate #

• `set.eq_on f₁ f₂ s` : functions `f₁` and `f₂` are equal at every point of `s`;
• `set.maps_to f s t` : `f` sends every point of `s` to a point of `t`;
• `set.inj_on f s` : restriction of `f` to `s` is injective;
• `set.surj_on f s t` : every point in `s` has a preimage in `s`;
• `set.bij_on f s t` : `f` is a bijection between `s` and `t`;
• `set.left_inv_on f' f s` : for every `x ∈ s` we have `f' (f x) = x`;
• `set.right_inv_on f' f t` : for every `y ∈ t` we have `f (f' y) = y`;
• `set.inv_on f' f s t` : `f'` is a two-side inverse of `f` on `s` and `t`, i.e. we have `set.left_inv_on f' f s` and `set.right_inv_on f' f t`.

Functions #

• `set.restrict f s` : restrict the domain of `f` to the set `s`;
• `set.cod_restrict f s h` : given `h : ∀ x, f x ∈ s`, restrict the codomain of `f` to the set `s`;
• `set.maps_to.restrict f s t h`: given `h : maps_to f s t`, restrict the domain of `f` to `s` and the codomain to `t`.

Restrict #

def set.restrict {α : Type u} {π : α → Type v} (s : set α) (f : Π (a : α), π a) (a : s) :
π a

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
theorem set.restrict_eq {α : Type u} {β : Type v} (f : α → β) (s : set α) :
@[simp]
theorem set.restrict_apply {α : Type u} {β : Type v} (f : α → β) (s : set α) (x : s) :
s.restrict f x = f x
theorem set.restrict_eq_iff {α : Type u} {π : α → Type v} {f : Π (a : α), π a} {s : set α} {g : Π (a : s), π a} :
s.restrict f = g ∀ (a : α) (ha : a s), f a = g a, ha⟩
theorem set.eq_restrict_iff {α : Type u} {π : α → Type v} {s : set α} {f : Π (a : s), π a} {g : Π (a : α), π a} :
f = s.restrict g ∀ (a : α) (ha : a s), f a, ha⟩ = g a
@[simp]
theorem set.range_restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) :
theorem set.image_restrict {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
s.restrict f '' (coe ⁻¹' t) = f '' (t s)
@[simp]
theorem set.restrict_dite {α : Type u} {β : Type v} {s : set α} [Π (x : α), decidable (x s)] (f : Π (a : α), a s → β) (g : Π (a : α), a s → β) :
s.restrict (λ (a : α), dite (a s) (λ (h : a s), f a h) (λ (h : a s), g a h)) = λ (a : s), f a _
@[simp]
theorem set.restrict_dite_compl {α : Type u} {β : Type v} {s : set α} [Π (x : α), decidable (x s)] (f : Π (a : α), a s → β) (g : Π (a : α), a s → β) :
s.restrict (λ (a : α), dite (a s) (λ (h : a s), f a h) (λ (h : a s), g a h)) = λ (a : s), g a _
@[simp]
theorem set.restrict_ite {α : Type u} {β : Type v} (f g : α → β) (s : set α) [Π (x : α), decidable (x s)] :
s.restrict (λ (a : α), ite (a s) (f a) (g a)) = s.restrict f
@[simp]
theorem set.restrict_ite_compl {α : Type u} {β : Type v} (f g : α → β) (s : set α) [Π (x : α), decidable (x s)] :
s.restrict (λ (a : α), ite (a s) (f a) (g a)) = s.restrict g
@[simp]
theorem set.restrict_piecewise {α : Type u} {β : Type v} (f g : α → β) (s : set α) [Π (x : α), decidable (x s)] :
@[simp]
theorem set.restrict_piecewise_compl {α : Type u} {β : Type v} (f g : α → β) (s : set α) [Π (x : α), decidable (x s)] :
theorem set.restrict_extend_range {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : α → γ) (g' : β → γ) :
(set.range f).restrict g g') = λ (x : (set.range f)), g (Exists.some _)
@[simp]
theorem set.restrict_extend_compl_range {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : α → γ) (g' : β → γ) :
theorem set.range_extend_subset {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : α → γ) (g' : β → γ) :
theorem set.range_extend {α : Type u} {β : Type v} {γ : Type w} {f : α → β} (hf : function.injective f) (g : α → γ) (g' : β → γ) :
def set.cod_restrict {α : Type u} {ι : Sort x} (f : ι → α) (s : set α) (h : ∀ (x : ι), f x s) :
ι → 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
• h = λ (x : ι), f x, _⟩
@[simp]
theorem set.coe_cod_restrict_apply {α : Type u} {ι : Sort x} (f : ι → α) (s : set α) (h : ∀ (x : ι), f x s) (x : ι) :
s h x) = f x
@[simp]
theorem set.restrict_comp_cod_restrict {α : Type u} {β : Type v} {ι : Sort x} {f : ι → α} {g : α → β} {b : set α} (h : ∀ (x : ι), f x b) :
b.restrict g h = g f
@[simp]
theorem set.injective_cod_restrict {α : Type u} {ι : Sort x} {f : ι → α} {s : set α} (h : ∀ (x : ι), f x s) :
theorem function.injective.cod_restrict {α : Type u} {ι : Sort x} {f : ι → α} {s : set α} (h : ∀ (x : ι), f x s) :

Alias of the reverse direction of `set.injective_cod_restrict`.

Equality on a set #

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
• f₂ s = ∀ ⦃x : α⦄, x sf₁ x = f₂ x
@[simp]
theorem set.eq_on_empty {α : Type u} {β : Type v} (f₁ f₂ : α → β) :
f₂
@[simp]
theorem set.restrict_eq_restrict_iff {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} :
s.restrict f₁ = s.restrict f₂ f₂ s
@[symm]
theorem set.eq_on.symm {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (h : f₂ s) :
f₁ s
theorem set.eq_on_comm {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} :
f₂ s f₁ s
@[refl]
theorem set.eq_on_refl {α : Type u} {β : Type v} (f : α → β) (s : set α) :
f s
@[trans]
theorem set.eq_on.trans {α : Type u} {β : Type v} {s : set α} {f₁ f₂ f₃ : α → β} (h₁ : f₂ s) (h₂ : f₃ s) :
f₃ s
theorem set.eq_on.image_eq {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (heq : f₂ s) :
f₁ '' s = f₂ '' s
theorem set.eq_on.inter_preimage_eq {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (heq : f₂ s) (t : set β) :
s f₁ ⁻¹' t = s f₂ ⁻¹' t
theorem set.eq_on.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {f₁ f₂ : α → β} (hs : s₁ s₂) (hf : f₂ s₂) :
f₂ s₁
theorem set.eq_on.comp_left {α : Type u} {β : Type v} {γ : Type w} {s : set α} {f₁ f₂ : α → β} {g : β → γ} (h : f₂ s) :
set.eq_on (g f₁) (g f₂) s
theorem set.comp_eq_of_eq_on_range {α : Type u} {β : Type v} {ι : Sort u_1} {f : ι → α} {g₁ g₂ : α → β} (h : g₂ (set.range f)) :
g₁ f = g₂ f

Congruence lemmas #

theorem monotone_on.congr {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h₁ : s) (h : f₂ s) :
s
theorem antitone_on.congr {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h₁ : s) (h : f₂ s) :
s
theorem strict_mono_on.congr {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h₁ : s) (h : f₂ s) :
s
theorem strict_anti_on.congr {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h₁ : s) (h : f₂ s) :
s
theorem set.eq_on.congr_monotone_on {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h : f₂ s) :
s s
theorem set.eq_on.congr_antitone_on {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h : f₂ s) :
s s
theorem set.eq_on.congr_strict_mono_on {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h : f₂ s) :
s s
theorem set.eq_on.congr_strict_anti_on {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} [preorder α] [preorder β] (h : f₂ s) :
s s

Mono lemmas #

theorem monotone_on.mono {α : Type u} {β : Type v} {s s₂ : set α} {f : α → β} [preorder α] [preorder β] (h : s) (h' : s₂ s) :
s₂
theorem antitone_on.mono {α : Type u} {β : Type v} {s s₂ : set α} {f : α → β} [preorder α] [preorder β] (h : s) (h' : s₂ s) :
s₂
theorem strict_mono_on.mono {α : Type u} {β : Type v} {s s₂ : set α} {f : α → β} [preorder α] [preorder β] (h : s) (h' : s₂ s) :
s₂
theorem strict_anti_on.mono {α : Type u} {β : Type v} {s s₂ : set α} {f : α → β} [preorder α] [preorder β] (h : s) (h' : s₂ s) :
s₂
@[protected]
theorem monotone_on.monotone {α : Type u} {β : Type v} {s : set α} {f : α → β} [preorder α] [preorder β] (h : s) :
@[protected]
theorem antitone_on.monotone {α : Type u} {β : Type v} {s : set α} {f : α → β} [preorder α] [preorder β] (h : s) :
@[protected]
theorem strict_mono_on.strict_mono {α : Type u} {β : Type v} {s : set α} {f : α → β} [preorder α] [preorder β] (h : s) :
@[protected]
theorem strict_anti_on.strict_anti {α : Type u} {β : Type v} {s : set α} {f : α → β} [preorder α] [preorder β] (h : s) :

maps to #

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
• s t = ∀ ⦃x : α⦄, x sf x t
def set.maps_to.restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) (h : s t) :
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
• t h = h
@[simp]
theorem set.maps_to.coe_restrict_apply {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) (x : s) :
t h x) = f x
theorem set.maps_to.coe_restrict {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
coe t h = s.restrict f
theorem set.maps_to.range_restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) (h : s t) :
set.range t h) = coe ⁻¹' (f '' s)
theorem set.maps_to_iff_exists_map_subtype {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
s t ∃ (g : s → t), ∀ (x : s), f x = (g x)
theorem set.maps_to' {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
s t f '' s t
@[simp]
theorem set.maps_to_singleton {α : Type u} {β : Type v} {t : set β} {f : α → β} {x : α} :
{x} t f x t
theorem set.maps_to_empty {α : Type u} {β : Type v} (f : α → β) (t : set β) :
t
theorem set.maps_to.image_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
f '' s t
theorem set.maps_to.congr {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h₁ : s t) (h : f₂ s) :
s t
theorem set.eq_on.comp_right {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f : α → β} {g₁ g₂ : β → γ} (hg : g₂ t) (hf : s t) :
set.eq_on (g₁ f) (g₂ f) s
theorem set.eq_on.maps_to_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (H : f₂ s) :
s t s t
theorem set.maps_to.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {p : set γ} {f : α → β} {g : β → γ} (h₁ : t p) (h₂ : s t) :
set.maps_to (g f) s p
theorem set.maps_to_id {α : Type u} (s : set α) :
s
theorem set.maps_to.iterate {α : Type u} {f : α → α} {s : set α} (h : s s) (n : ) :
s s
theorem set.maps_to.iterate_restrict {α : Type u} {f : α → α} {s : set α} (h : s s) (n : ) :
s h^[n] = s _
theorem set.maps_to.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (hf : s₁ t₁) (hs : s₂ s₁) (ht : t₁ t₂) :
s₂ t₂
theorem set.maps_to.mono_left {α : Type u} {β : Type v} {s₁ s₂ : set α} {t : set β} {f : α → β} (hf : s₁ t) (hs : s₂ s₁) :
s₂ t
theorem set.maps_to.mono_right {α : Type u} {β : Type v} {s : set α} {t₁ t₂ : set β} {f : α → β} (hf : s t₁) (ht : t₁ t₂) :
s t₂
theorem set.maps_to.union_union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
(s₁ s₂) (t₁ t₂)
theorem set.maps_to.union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t : set β} {f : α → β} (h₁ : s₁ t) (h₂ : s₂ t) :
(s₁ s₂) t
@[simp]
theorem set.maps_to_union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t : set β} {f : α → β} :
(s₁ s₂) t s₁ t s₂ t
theorem set.maps_to.inter {α : Type u} {β : Type v} {s : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s t₁) (h₂ : s t₂) :
s (t₁ t₂)
theorem set.maps_to.inter_inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
(s₁ s₂) (t₁ t₂)
@[simp]
theorem set.maps_to_inter {α : Type u} {β : Type v} {s : set α} {t₁ t₂ : set β} {f : α → β} :
s (t₁ t₂) s t₁ s t₂
theorem set.maps_to_univ {α : Type u} {β : Type v} (f : α → β) (s : set α) :
theorem set.maps_to_image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s (f '' s)
theorem set.maps_to_preimage {α : Type u} {β : Type v} (f : α → β) (t : set β) :
(f ⁻¹' t) t
theorem set.maps_to_range {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s (set.range f)
@[simp]
theorem set.maps_image_to {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : γ → α) (s : set γ) (t : set β) :
(g '' s) t set.maps_to (f g) s t
@[simp]
theorem set.maps_univ_to {α : Type u} {β : Type v} (f : α → β) (s : set β) :
∀ (a : α), f a s
@[simp]
theorem set.maps_range_to {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : γ → α) (s : set β) :
theorem set.surjective_maps_to_image_restrict {α : Type u} {β : Type v} (f : α → β) (s : set α) :
theorem set.maps_to.mem_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) (hc : s t) {x : α} :
f x t x s

Restriction onto preimage #

@[simp]
theorem set.restrict_preimage_coe {α : Type u} {β : Type v} (t : set β) (f : α → β) (ᾰ : (f ⁻¹' t)) :
ᾰ) = f
def set.restrict_preimage {α : Type u} {β : Type v} (t : set β) (f : α → β) :
(f ⁻¹' t)t

The restriction of a function onto the preimage of a set.

Equations
theorem set.range_restrict_preimage {α : Type u} {β : Type v} (t : set β) (f : α → β) :
=

Injectivity on a set #

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
• s = ∀ ⦃x₁ : α⦄, x₁ s∀ ⦃x₂ : α⦄, x₂ sf x₁ = f x₂x₁ = x₂
theorem set.subsingleton.inj_on {α : Type u} {β : Type v} {s : set α} (hs : s.subsingleton) (f : α → β) :
s
@[simp]
theorem set.inj_on_empty {α : Type u} {β : Type v} (f : α → β) :
@[simp]
theorem set.inj_on_singleton {α : Type u} {β : Type v} (f : α → β) (a : α) :
{a}
theorem set.inj_on.eq_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} {x y : α} (h : s) (hx : x s) (hy : y s) :
f x = f y x = y
theorem set.inj_on.congr {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (h₁ : s) (h : f₂ s) :
s
theorem set.eq_on.inj_on_iff {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} (H : f₂ s) :
s s
theorem set.inj_on.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {f : α → β} (h : s₁ s₂) (ht : s₂) :
s₁
theorem set.inj_on_union {α : Type u} {β : Type v} {s₁ s₂ : set α} {f : α → β} (h : disjoint s₁ s₂) :
(s₁ s₂) s₁ s₂ ∀ (x : α), x s₁∀ (y : α), y s₂f x f y
theorem set.inj_on_insert {α : Type u} {β : Type v} {f : α → β} {s : set α} {a : α} (has : a s) :
s) s f a f '' s
theorem set.injective_iff_inj_on_univ {α : Type u} {β : Type v} {f : α → β} :
theorem set.inj_on_of_injective {α : Type u} {β : Type v} {f : α → β} (h : function.injective f) (s : set α) :
s
theorem function.injective.inj_on {α : Type u} {β : Type v} {f : α → β} (h : function.injective f) (s : set α) :
s

Alias of `set.inj_on_of_injective`.

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

Alias of the forward direction of `set.inj_on_iff_injective`.

theorem set.exists_inj_on_iff_injective {α : Type u} {β : Type v} {s : set α} [nonempty β] :
(∃ (f : α → β), s) ∃ (f : s → β),
theorem set.inj_on_preimage {α : Type u} {β : Type v} {f : α → β} {B : set (set β)} (hB : B ) :
B
theorem set.inj_on.mem_of_mem_image {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} {x : α} (hf : s) (hs : s₁ s) (h : x s) (h₁ : f x f '' s₁) :
x s₁
theorem set.inj_on.mem_image_iff {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} {x : α} (hf : s) (hs : s₁ s) (hx : x s) :
f x f '' s₁ x s₁
theorem set.inj_on.preimage_image_inter {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} (hf : s) (hs : s₁ s) :
f ⁻¹' (f '' s₁) s = s₁
theorem set.eq_on.cancel_left {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f₁ f₂ : α → β} {g : β → γ} (h : set.eq_on (g f₁) (g f₂) s) (hg : t) (hf₁ : s t) (hf₂ : s t) :
f₂ s
theorem set.inj_on.cancel_left {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f₁ f₂ : α → β} {g : β → γ} (hg : t) (hf₁ : s t) (hf₂ : s t) :
set.eq_on (g f₁) (g f₂) s f₂ s

Surjectivity on a set #

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
theorem set.surj_on.subset_range {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
t
theorem set.surj_on_iff_exists_map_subtype {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
s t ∃ (t' : set β) (g : s → t'), t t' ∀ (x : s), f x = (g x)
theorem set.surj_on_empty {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s
theorem set.surj_on_image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s (f '' s)
theorem set.surj_on.comap_nonempty {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) (ht : t.nonempty) :
theorem set.surj_on.congr {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h : s t) (H : f₂ s) :
s t
theorem set.eq_on.surj_on_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h : f₂ s) :
s t s t
theorem set.surj_on.mono {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (hs : s₁ s₂) (ht : t₁ t₂) (hf : s₁ t₂) :
s₂ t₁
theorem set.surj_on.union {α : Type u} {β : Type v} {s : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s t₁) (h₂ : s t₂) :
s (t₁ t₂)
theorem set.surj_on.union_union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
(s₁ s₂) (t₁ t₂)
theorem set.surj_on.inter_inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s₁ t₁) (h₂ : s₂ t₂) (h : (s₁ s₂)) :
(s₁ s₂) (t₁ t₂)
theorem set.surj_on.inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t : set β} {f : α → β} (h₁ : s₁ t) (h₂ : s₂ t) (h : (s₁ s₂)) :
(s₁ s₂) t
theorem set.surj_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {p : set γ} {f : α → β} {g : β → γ} (hg : t p) (hf : s t) :
set.surj_on (g f) s p
theorem set.surjective_iff_surj_on_univ {α : Type u} {β : Type v} {f : α → β} :
theorem set.surj_on_iff_surjective {α : Type u} {β : Type v} {s : set α} {f : α → β} :
theorem set.surj_on.image_eq_of_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h₁ : s t) (h₂ : s t) :
f '' s = t
theorem set.image_eq_iff_surj_on_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
f '' s = t s t s t
theorem set.surj_on.maps_to_compl {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) (h' : function.injective f) :
s t
theorem set.maps_to.surj_on_compl {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) (h' : function.surjective f) :
s t
theorem set.eq_on.cancel_right {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f : α → β} {g₁ g₂ : β → γ} (hf : set.eq_on (g₁ f) (g₂ f) s) (hf' : s t) :
g₂ t
theorem set.surj_on.cancel_right {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f : α → β} {g₁ g₂ : β → γ} (hf : s t) (hf' : s t) :
set.eq_on (g₁ f) (g₂ f) s g₂ t
theorem set.eq_on_comp_right_iff {α : Type u} {β : Type v} {γ : Type w} {s : set α} {f : α → β} {g₁ g₂ : β → γ} :
set.eq_on (g₁ f) (g₂ f) s g₂ (f '' s)

Bijectivity #

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
theorem set.bij_on.maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
s t
theorem set.bij_on.inj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
s
theorem set.bij_on.surj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
s t
theorem set.bij_on.mk {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h₁ : s t) (h₂ : s) (h₃ : s t) :
s t
theorem set.bij_on_empty {α : Type u} {β : Type v} (f : α → β) :
theorem set.bij_on.inter {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s₁ t₁) (h₂ : s₂ t₂) (h : (s₁ s₂)) :
(s₁ s₂) (t₁ t₂)
theorem set.bij_on.union {α : Type u} {β : Type v} {s₁ s₂ : set α} {t₁ t₂ : set β} {f : α → β} (h₁ : s₁ t₁) (h₂ : s₂ t₂) (h : (s₁ s₂)) :
(s₁ s₂) (t₁ t₂)
theorem set.bij_on.subset_range {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
t
theorem set.inj_on.bij_on_image {α : Type u} {β : Type v} {s : set α} {f : α → β} (h : s) :
s (f '' s)
theorem set.bij_on.congr {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (h₁ : s t) (h : f₂ s) :
s t
theorem set.eq_on.bij_on_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} (H : f₂ s) :
s t s t
theorem set.bij_on.image_eq {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
f '' s = t
theorem set.bij_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {p : set γ} {f : α → β} {g : β → γ} (hg : t p) (hf : s t) :
set.bij_on (g f) s p
theorem set.bij_on.bijective {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (h : s t) :
theorem set.bijective_iff_bij_on_univ {α : Type u} {β : Type v} {f : α → β} :
theorem set.bij_on.compl {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (hst : s t) (hf : function.bijective f) :
s t

left inverse #

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
• f s = ∀ ⦃x : α⦄, x sf' (f x) = x
theorem set.left_inv_on.eq_on {α : Type u} {β : Type v} {s : set α} {f : α → β} {f' : β → α} (h : f s) :
set.eq_on (f' f) id s
theorem set.left_inv_on.eq {α : Type u} {β : Type v} {s : set α} {f : α → β} {f' : β → α} (h : f s) {x : α} (hx : x s) :
f' (f x) = x
theorem set.left_inv_on.congr_left {α : Type u} {β : Type v} {s : set α} {f : α → β} {f₁' f₂' : β → α} (h₁ : f s) {t : set β} (h₁' : s t) (heq : set.eq_on f₁' f₂' t) :
f s
theorem set.left_inv_on.congr_right {α : Type u} {β : Type v} {s : set α} {f₁ f₂ : α → β} {f₁' : β → α} (h₁ : f₁ s) (heq : f₂ s) :
f₂ s
theorem set.left_inv_on.inj_on {α : Type u} {β : Type v} {s : set α} {f : α → β} {f₁' : β → α} (h : f s) :
s
theorem set.left_inv_on.surj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : f s) (hf : s t) :
t s
theorem set.left_inv_on.maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : f s) (hf : s t) :
t s
theorem set.left_inv_on.comp {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf' : f s) (hg' : g t) (hf : s t) :
set.left_inv_on (f' g') (g f) s
theorem set.left_inv_on.mono {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} {f' : β → α} (hf : f s) (ht : s₁ s) :
f s₁
theorem set.left_inv_on.image_inter' {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} {f' : β → α} (hf : f s) :
f '' (s₁ s) = f' ⁻¹' s₁ f '' s
theorem set.left_inv_on.image_inter {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} {f' : β → α} (hf : f s) :
f '' (s₁ s) = f' ⁻¹' (s₁ s) f '' s
theorem set.left_inv_on.image_image {α : Type u} {β : Type v} {s : set α} {f : α → β} {f' : β → α} (hf : f s) :
f' '' (f '' s) = s
theorem set.left_inv_on.image_image' {α : Type u} {β : Type v} {s s₁ : set α} {f : α → β} {f' : β → α} (hf : f s) (hs : s₁ s) :
f' '' (f '' s₁) = s₁

Right inverse #

@[reducible]
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
• f t = f' t
theorem set.right_inv_on.eq_on {α : Type u} {β : Type v} {t : set β} {f : α → β} {f' : β → α} (h : f t) :
set.eq_on (f f') id t
theorem set.right_inv_on.eq {α : Type u} {β : Type v} {t : set β} {f : α → β} {f' : β → α} (h : f t) {y : β} (hy : y t) :
f (f' y) = y
theorem set.left_inv_on.right_inv_on_image {α : Type u} {β : Type v} {s : set α} {f : α → β} {f' : β → α} (h : f s) :
f (f '' s)
theorem set.right_inv_on.congr_left {α : Type u} {β : Type v} {t : set β} {f : α → β} {f₁' f₂' : β → α} (h₁ : f t) (heq : set.eq_on f₁' f₂' t) :
f t
theorem set.right_inv_on.congr_right {α : Type u} {β : Type v} {s : set α} {t : set β} {f₁ f₂ : α → β} {f' : β → α} (h₁ : f₁ t) (hg : t s) (heq : f₂ s) :
f₂ t
theorem set.right_inv_on.surj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (hf : f t) (hf' : t s) :
s t
theorem set.right_inv_on.maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : f t) (hf : t s) :
s t
theorem set.right_inv_on.comp {α : Type u} {β : Type v} {γ : Type w} {t : set β} {p : set γ} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf : f t) (hg : g p) (g'pt : p t) :
set.right_inv_on (f' g') (g f) p
theorem set.right_inv_on.mono {α : Type u} {β : Type v} {t t₁ : set β} {f : α → β} {f' : β → α} (hf : f t) (ht : t₁ t) :
f t₁
theorem set.inj_on.right_inv_on_of_left_inv_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (hf : s) (hf' : f' t) (h₁ : s t) (h₂ : t s) :
f' s
theorem set.eq_on_of_left_inv_on_of_right_inv_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f₁' f₂' : β → α} (h₁ : f s) (h₂ : f t) (h : set.maps_to f₂' t s) :
set.eq_on f₁' f₂' t
theorem set.surj_on.left_inv_on_of_right_inv_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (hf : s t) (hf' : f' s) :
f' t

Two-side inverses #

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
• f s t = f s t)
theorem set.inv_on.symm {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : f s t) :
f' t s
theorem set.inv_on.mono {α : Type u} {β : Type v} {s s₁ : set α} {t t₁ : set β} {f : α → β} {f' : β → α} (h : f s t) (hs : s₁ s) (ht : t₁ t) :
f s₁ t₁
theorem set.inv_on.bij_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {f' : β → α} (h : f s t) (hf : s t) (hf' : t s) :
s t

If functions `f'` and `f` are inverse on `s` and `t`, `f` maps `s` into `t`, and `f'` maps `t` into `s`, then `f` is a bijection between `s` and `t`. The `maps_to` arguments can be deduced from `surj_on` statements using `left_inv_on.maps_to` and `right_inv_on.maps_to`.

`inv_fun_on` is a left/right inverse #

noncomputable def function.inv_fun_on {α : Type u} {β : Type v} [nonempty α] (f : α → β) (s : set α) (b : β) :
α

Construct the inverse for a function `f` on domain `s`. This function is a right inverse of `f` on `f '' s`. For a computable version, see `function.injective.inv_of_mem_range`.

Equations
theorem function.inv_fun_on_pos {α : Type u} {β : Type v} [nonempty α] {s : set α} {f : α → β} {b : β} (h : ∃ (a : α) (H : a s), f a = b) :
b s f b) = b
theorem function.inv_fun_on_mem {α : Type u} {β : Type v} [nonempty α] {s : set α} {f : α → β} {b : β} (h : ∃ (a : α) (H : a s), f a = b) :
b s
theorem function.inv_fun_on_eq {α : Type u} {β : Type v} [nonempty α] {s : set α} {f : α → β} {b : β} (h : ∃ (a : α) (H : a s), f a = b) :
f b) = b
theorem function.inv_fun_on_neg {α : Type u} {β : Type v} [nonempty α] {s : set α} {f : α → β} {b : β} (h : ¬∃ (a : α) (H : a s), f a = b) :
b = classical.choice _inst_1
theorem set.inj_on.left_inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {f : α → β} [nonempty α] (h : s) :
s
theorem set.inj_on.inv_fun_on_image {α : Type u} {β : Type v} {s₁ s₂ : set α} {f : α → β} [nonempty α] (h : s₂) (ht : s₁ s₂) :
'' (f '' s₁) = s₁
theorem set.surj_on.right_inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : s t) :
t
theorem set.bij_on.inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : s t) :
f s t
theorem set.surj_on.inv_on_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : s t) :
f '' t) t
theorem set.surj_on.maps_to_inv_fun_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : s t) :
t s
theorem set.surj_on.bij_on_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} [nonempty α] (h : s t) :
'' t) t
theorem set.surj_on_iff_exists_bij_on_subset {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
s t ∃ (s' : set α) (H : s' s), s' t
theorem set.preimage_inv_fun_of_mem {α : Type u} {β : Type v} [n : nonempty α] {f : α → β} (hf : function.injective f) {s : set α} (h : s) :
= f '' s (set.range f)
theorem set.preimage_inv_fun_of_not_mem {α : Type u} {β : Type v} [n : nonempty α] {f : α → β} (hf : function.injective f) {s : set α} (h : s) :
= f '' s

Monotone #

@[protected]
theorem monotone.restrict {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : monotone f) (s : set α) :
@[protected]
theorem monotone.cod_restrict {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : monotone f) {s : set β} (hs : ∀ (x : α), f x s) :
monotone s hs)
@[protected]
theorem monotone.range_factorization {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (h : monotone f) :

Piecewise defined function #

@[simp]
theorem set.piecewise_empty {α : Type u} {δ : α → Sort y} (f g : Π (i : α), δ i) [Π (i : α), decidable (i )] :
g = g
@[simp]
theorem set.piecewise_univ {α : Type u} {δ : α → Sort y} (f g : Π (i : α), δ i) [Π (i : α), decidable (i set.univ)] :
= f
@[simp]
theorem set.piecewise_insert_self {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) {j : α} [Π (i : α), decidable (i ] :
s).piecewise f g j = f j
@[protected, instance]
def set.compl.decidable_mem {α : Type u} (s : set α) [Π (j : α), decidable (j s)] (j : α) :
Equations
theorem set.piecewise_insert {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] [decidable_eq α] (j : α) [Π (i : α), decidable (i ] :
s).piecewise f g = function.update (s.piecewise f g) j (f j)
@[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
@[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
theorem set.piecewise_singleton {α : Type u} {β : Type v} (x : α) [Π (y : α), decidable (y {x})] [decidable_eq α] (f g : α → β) :
{x}.piecewise f g = (f x)
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
theorem set.piecewise_eq_on_compl {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j s)] (f g : α → β) :
theorem set.piecewise_le {α : Type u} {δ : α → Type u_1} [Π (i : α), preorder (δ i)] {s : set α} [Π (j : α), decidable (j s)] {f₁ f₂ g : Π (i : α), δ i} (h₁ : ∀ (i : α), i sf₁ i g i) (h₂ : ∀ (i : α), i sf₂ i g i) :
s.piecewise f₁ f₂ g
theorem set.le_piecewise {α : Type u} {δ : α → Type u_1} [Π (i : α), preorder (δ i)] {s : set α} [Π (j : α), decidable (j s)] {f₁ f₂ g : Π (i : α), δ i} (h₁ : ∀ (i : α), i sg i f₁ i) (h₂ : ∀ (i : α), i sg i f₂ i) :
g s.piecewise f₁ f₂
theorem set.piecewise_le_piecewise {α : Type u} {δ : α → Type u_1} [Π (i : α), preorder (δ i)] {s : set α} [Π (j : α), decidable (j s)] {f₁ f₂ g₁ g₂ : Π (i : α), δ i} (h₁ : ∀ (i : α), i sf₁ i g₁ i) (h₂ : ∀ (i : α), i sf₂ i g₂ i) :
s.piecewise f₁ f₂ s.piecewise g₁ g₂
@[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 ] :
s).piecewise f g i = s.piecewise f g i
@[simp]
theorem set.piecewise_compl {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] [Π (i : α), decidable (i s)] :
@[simp]
theorem set.piecewise_range_comp {α : Type u} {β : Type v} {ι : Sort u_1} (f : ι → α) [Π (j : α), decidable (j ] (g₁ g₂ : α → β) :
(set.range f).piecewise g₁ g₂ f = g₁ f
theorem set.maps_to.piecewise_ite {α : Type u} {β : Type v} {s s₁ s₂ : set α} {t t₁ t₂ : set β} {f₁ f₂ : α → β} [Π (i : α), decidable (i s)] (h₁ : (s₁ s) (t₁ t)) (h₂ : (s₂ s) (t₂ t)) :
set.maps_to (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
theorem set.eq_on_piecewise {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j s)] {f f' g : α → β} {t : set α} :
set.eq_on (s.piecewise f f') g t g (t s) g (t s)
theorem set.eq_on.piecewise_ite' {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j s)] {f f' g : α → β} {t t' : set α} (h : g (t s)) (h' : g (t' s)) :
set.eq_on (s.piecewise f f') g (s.ite t t')
theorem set.eq_on.piecewise_ite {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j s)] {f f' g : α → β} {t t' : set α} (h : g t) (h' : g t') :
set.eq_on (s.piecewise f f') g (s.ite t t')
theorem set.piecewise_preimage {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j s)] (f g : α → β) (t : set β) :
s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t)
theorem set.apply_piecewise {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] {δ' : α → Sort u_1} (h : Π (i : α), δ iδ' i) {x : α} :
h x (s.piecewise f g x) = s.piecewise (λ (x : α), h x (f x)) (λ (x : α), h x (g x)) x
theorem set.apply_piecewise₂ {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] {δ' : α → Sort u_1} {δ'' : α → Sort u_2} (f' g' : Π (i : α), δ' i) (h : Π (i : α), δ iδ' iδ'' i) {x : α} :
h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (λ (x : α), h x (f x) (f' x)) (λ (x : α), h x (g x) (g' x)) x
theorem set.piecewise_op {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] {δ' : α → Sort u_1} (h : Π (i : α), δ iδ' i) :
s.piecewise (λ (x : α), h x (f x)) (λ (x : α), h x (g x)) = λ (x : α), h x (s.piecewise f g x)
theorem set.piecewise_op₂ {α : Type u} {δ : α → Sort y} (s : set α) (f g : Π (i : α), δ i) [Π (j : α), decidable (j s)] {δ' : α → Sort u_1} {δ'' : α → Sort u_2} (f' g' : Π (i : α), δ' i) (h : Π (i : α), δ iδ' iδ'' i) :
s.piecewise (λ (x : α), h x (f x) (f' x)) (λ (x : α), h x (g x) (g' x)) = λ (x : α), h x (s.piecewise f g x) (s.piecewise f' g' x)
@[simp]
theorem set.piecewise_same {α : Type u} {δ : α → Sort y} (s : set α) (f : Π (i : α), δ i) [Π (j : α), decidable (j s)] :
s.piecewise f f = f
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
theorem set.injective_piecewise_iff {α : Type u} {β : Type v} (s : set α) [Π (j : α), decidable (j s)] {f g : α → β} :
function.injective (s.piecewise f g) s s ∀ (x : α), x s∀ (y : α), y sf x g y
theorem set.piecewise_mem_pi {α : Type u} (s : set α) [Π (j : α), decidable (j s)] {δ : α → Type u_1} {t : set α} {t' : Π (i : α), set (δ i)} {f g : Π (i : α), δ i} (hf : f t.pi t') (hg : g t.pi t') :
s.piecewise f g t.pi t'
@[simp]
theorem set.pi_piecewise {ι : Type u_1} {α : ι → Type u_2} (s s' : set ι) (t t' : Π (i : ι), set (α i)) [Π (x : ι), decidable (x s')] :
s.pi (s'.piecewise t t') = (s s').pi t (s \ s').pi t'
theorem set.univ_pi_piecewise {ι : Type u_1} {α : ι → Type u_2} (s : set ι) (t : Π (i : ι), set (α i)) [Π (x : ι), decidable (x s)] :
set.univ.pi (s.piecewise t (λ (_x : ι), set.univ)) = s.pi t
theorem strict_mono_on.inj_on {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} (H : s) :
s
theorem strict_anti_on.inj_on {α : Type u} {β : Type v} [linear_order α] [preorder β] {f : α → β} {s : set α} (H : s) :
s
theorem strict_mono_on.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : t) (hf : s) (hs : s t) :
theorem strict_mono_on.comp_strict_anti_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : t) (hf : s) (hs : s t) :
theorem strict_anti_on.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : t) (hf : s) (hs : s t) :
theorem strict_anti_on.comp_strict_mono_on {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : t) (hf : s) (hs : s t) :
theorem strict_mono.cod_restrict {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) {s : set β} (hs : ∀ (x : α), f x s) :
theorem function.injective.comp_inj_on {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {s : set α} (hg : function.injective g) (hf : s) :
set.inj_on (g f) s
theorem function.surjective.surj_on {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) (s : set β) :
theorem function.left_inverse.left_inv_on {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : g) (s : set β) :
s
theorem function.right_inverse.right_inv_on {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : g) (s : set α) :
s
theorem function.left_inverse.right_inv_on_range {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : g) :
theorem function.semiconj.maps_to_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s t : set α} (h : fb) (ha : s t) :
(f '' s) (f '' t)
theorem function.semiconj.maps_to_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : fb) :
theorem function.semiconj.surj_on_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s t : set α} (h : fb) (ha : s t) :
(f '' s) (f '' t)
theorem function.semiconj.surj_on_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : fb) (ha : function.surjective fa) :
theorem function.semiconj.inj_on_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s : set α} (h : fb) (ha : s) (hf : (fa '' s)) :
(f '' s)
theorem function.semiconj.inj_on_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : fb) (ha : function.injective fa) (hf : (set.range fa)) :
theorem function.semiconj.bij_on_image {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} {s t : set α} (h : fb) (ha : s t) (hf : t) :
(f '' s) (f '' t)
theorem function.semiconj.bij_on_range {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : fb) (ha : function.bijective fa) (hf : function.injective f) :
theorem function.semiconj.maps_to_preimage {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : fb) {s t : set β} (hb : s t) :
(f ⁻¹' s) (f ⁻¹' t)
theorem function.semiconj.inj_on_preimage {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {f : α → β} (h : fb) {s : set β} (hb : s) (hf : (f ⁻¹' s)) :
(f ⁻¹' s)
theorem function.update_comp_eq_of_not_mem_range' {α : Sort u_1} {β : Type u_2} {γ : β → Sort u_3} [decidable_eq β] (g : Π (b : β), γ b) {f : α → β} {i : β} (a : γ i) (h : i ) :
(λ (j : α), a (f j)) = λ (j : α), g (f j)
theorem function.update_comp_eq_of_not_mem_range {α : Sort u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq β] (g : β → γ) {f : α → β} {i : β} (a : γ) (h : i ) :
a f = g f

Non-dependent version of `function.update_comp_eq_of_not_mem_range'`

theorem function.insert_inj_on {α : Type u} (s : set α) :
set.inj_on (λ (a : α), s