Functions over sets
Main definitions
Predicate
eq_on f₁ f₂ s: functionsf₁andf₂are equal at every point ofs;maps_to f s t:fsends every point ofsto a point oft;inj_on f s: restriction offtosis injective;surj_on f s t: every point inshas a preimage ins;bij_on f s t:fis a bijection betweensandt;left_inv_on f' f s: for everyx ∈ swe havef' (f x) = x;right_inv_on f' f t: for everyy ∈ twe havef (f' y) = y;inv_on f' f s t:f'is a two-side inverse offonsandt, i.e. we haveleft_inv_on f' f sandright_inv_on f' f t.
Functions
restrict f s: restrict the domain offto the sets;cod_restrict f s h: givenh : ∀ x, f x ∈ s, restrict the codomain offto the sets;maps_to.restrict f s t h: givenh : maps_to f s t, restrict the domain offtosand the codomain tot.
Restrict
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
- set.restrict f s = λ (x : ↥s), f ↑x
theorem
set.restrict_eq
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.restrict f s = f ∘ coe
@[simp]
theorem
set.restrict_apply
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α)
(x : ↥s) :
set.restrict f s x = f ↑x
@[simp]
theorem
set.range_restrict
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.range (set.restrict f s) = f '' 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
- set.cod_restrict f s h = λ (x : α), ⟨f x, _⟩
@[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
maps to
maps_to f a b means that the image of a is contained in b.
Equations
- set.maps_to f s t = ∀ ⦃x : α⦄, x ∈ s → f x ∈ t
def
set.maps_to.restrict
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α)
(t : set β) :
set.maps_to f 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
- set.maps_to.restrict f s t h = subtype.map f h
@[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
theorem
set.maps_to'
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.maps_to f s t ↔ f '' s ⊆ t
theorem
set.maps_to.image_subset
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.maps_to f s t → f '' s ⊆ t
theorem
set.maps_to.congr
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β} :
set.maps_to f₁ s t → set.eq_on f₁ f₂ s → set.maps_to f₂ s t
theorem
set.eq_on.maps_to_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β} :
set.eq_on f₁ f₂ s → (set.maps_to f₁ s t ↔ set.maps_to f₂ s t)
theorem
set.maps_to.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ} :
set.maps_to g t p → set.maps_to f s t → set.maps_to (g ∘ f) s p
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
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 _
theorem
set.maps_to.mono
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
s₂ ⊆ s₁ → t₁ ⊆ t₂ → set.maps_to f s₁ t₁ → set.maps_to f s₂ t₂
theorem
set.maps_to.union_union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.maps_to f s₁ t₁ → set.maps_to f s₂ t₂ → set.maps_to f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
set.maps_to.union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t : set β}
{f : α → β} :
set.maps_to f s₁ t → set.maps_to f s₂ t → set.maps_to f (s₁ ∪ s₂) t
theorem
set.maps_to.inter
{α : Type u}
{β : Type v}
{s : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.maps_to f s t₁ → set.maps_to f s t₂ → set.maps_to f s (t₁ ∩ t₂)
theorem
set.maps_to.inter_inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.maps_to f s₁ t₁ → set.maps_to f s₂ t₂ → set.maps_to f (s₁ ∩ s₂) (t₁ ∩ t₂)
theorem
set.maps_to_univ
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.maps_to f s set.univ
theorem
set.maps_to_image
{α : Type u}
{β : Type v}
(f : α → β)
(s : set α) :
set.maps_to f s (f '' s)
theorem
set.maps_to_preimage
{α : Type u}
{β : Type v}
(f : α → β)
(t : set β) :
set.maps_to f (f ⁻¹' t) t
Injectivity on a set
f is injective on a if the restriction of f to a is injective.
theorem
set.inj_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β} :
set.inj_on f₁ s → set.eq_on f₁ f₂ s → set.inj_on f₂ s
theorem
set.eq_on.inj_on_iff
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β} :
set.eq_on f₁ f₂ s → (set.inj_on f₁ s ↔ set.inj_on f₂ s)
theorem
set.inj_on.mono
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{f : α → β} :
s₁ ⊆ s₂ → set.inj_on f s₂ → set.inj_on f s₁
theorem
set.inj_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g : β → γ} :
set.inj_on g t → set.inj_on f s → set.maps_to f s t → set.inj_on (g ∘ f) s
theorem
set.inj_on_iff_injective
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s ↔ function.injective (set.restrict f s)
theorem
set.inj_on.inv_fun_on_image
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{f : α → β}
[nonempty α] :
set.inj_on f s₂ → s₁ ⊆ s₂ → function.inv_fun_on f s₂ '' (f '' s₁) = s₁
theorem
set.inj_on_preimage
{α : Type u}
{β : Type v}
{f : α → β}
{B : set (set β)} :
B ⊆ 𝒫set.range f → set.inj_on (set.preimage f) B
Surjectivity on a set
f is surjective from a to b if b is contained in the image of a.
Equations
- set.surj_on f s t = (t ⊆ f '' s)
theorem
set.surj_on.subset_range
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.surj_on f s t → t ⊆ set.range f
theorem
set.surj_on.comap_nonempty
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.surj_on f s t → t.nonempty → s.nonempty
theorem
set.surj_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β} :
set.surj_on f₁ s t → set.eq_on f₁ f₂ s → set.surj_on f₂ s t
theorem
set.eq_on.surj_on_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β} :
set.eq_on f₁ f₂ s → (set.surj_on f₁ s t ↔ set.surj_on f₂ s t)
theorem
set.surj_on.mono
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
s₁ ⊆ s₂ → t₁ ⊆ t₂ → set.surj_on f s₁ t₂ → set.surj_on f s₂ t₁
theorem
set.surj_on.union
{α : Type u}
{β : Type v}
{s : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.surj_on f s t₁ → set.surj_on f s t₂ → set.surj_on f s (t₁ ∪ t₂)
theorem
set.surj_on.union_union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.surj_on f s₁ t₁ → set.surj_on f s₂ t₂ → set.surj_on f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
set.surj_on.inter_inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.surj_on f s₁ t₁ → set.surj_on f s₂ t₂ → set.inj_on f (s₁ ∪ s₂) → set.surj_on f (s₁ ∩ s₂) (t₁ ∩ t₂)
theorem
set.surj_on.inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t : set β}
{f : α → β} :
set.surj_on f s₁ t → set.surj_on f s₂ t → set.inj_on f (s₁ ∪ s₂) → set.surj_on f (s₁ ∩ s₂) t
theorem
set.surj_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ} :
set.surj_on g t p → set.surj_on f s t → set.surj_on (g ∘ f) s p
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)
theorem
set.surj_on.image_eq_of_maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.surj_on f s t → set.maps_to f s t → f '' s = t
Bijectivity
f is bijective from s to t if f is injective on s and f '' s = t.
Equations
- set.bij_on f s t = (set.maps_to f s t ∧ set.inj_on f s ∧ set.surj_on f s t)
theorem
set.bij_on.maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.bij_on f s t → set.maps_to f s t
theorem
set.bij_on.inj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.bij_on f s t → set.inj_on f s
theorem
set.bij_on.surj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.bij_on f s t → set.surj_on f s t
theorem
set.bij_on.mk
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.maps_to f s t → set.inj_on f s → set.surj_on f s t → set.bij_on f s t
theorem
set.bij_on.inter
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.bij_on f s₁ t₁ → set.bij_on f s₂ t₂ → set.inj_on f (s₁ ∪ s₂) → set.bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂)
theorem
set.bij_on.union
{α : Type u}
{β : Type v}
{s₁ s₂ : set α}
{t₁ t₂ : set β}
{f : α → β} :
set.bij_on f s₁ t₁ → set.bij_on f s₂ t₂ → set.inj_on f (s₁ ∪ s₂) → set.bij_on f (s₁ ∪ s₂) (t₁ ∪ t₂)
theorem
set.bij_on.subset_range
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.bij_on f s t → t ⊆ set.range f
theorem
set.inj_on.bij_on_image
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s → set.bij_on f s (f '' s)
theorem
set.bij_on.congr
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β} :
set.bij_on f₁ s t → set.eq_on f₁ f₂ s → set.bij_on f₂ s t
theorem
set.eq_on.bij_on_iff
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β} :
set.eq_on f₁ f₂ s → (set.bij_on f₁ s t ↔ set.bij_on f₂ s t)
theorem
set.bij_on.image_eq
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β} :
set.bij_on f s t → f '' s = t
theorem
set.bij_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ} :
set.bij_on g t p → set.bij_on f s t → set.bij_on (g ∘ f) s p
left inverse
g is a left inverse to f on a means that g (f x) = x for all x ∈ a.
Equations
- set.left_inv_on f' f s = ∀ ⦃x : α⦄, x ∈ s → f' (f x) = x
theorem
set.left_inv_on.eq_on
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f' : β → α} :
set.left_inv_on f' f s → set.eq_on (f' ∘ f) id s
theorem
set.left_inv_on.eq
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f' : β → α}
(h : set.left_inv_on f' f s)
{x : α} :
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 β} :
set.maps_to f s t → set.eq_on f₁' f₂' t → set.left_inv_on f₂' f s
theorem
set.left_inv_on.congr_right
{α : Type u}
{β : Type v}
{s : set α}
{f₁ f₂ : α → β}
{f₁' : β → α} :
set.left_inv_on f₁' f₁ s → set.eq_on f₁ f₂ s → set.left_inv_on f₁' f₂ s
theorem
set.left_inv_on.inj_on
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
{f₁' : β → α} :
set.left_inv_on f₁' f s → set.inj_on f s
theorem
set.left_inv_on.surj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f₁' : β → α} :
set.left_inv_on f₁' f s → set.maps_to f s t → set.surj_on f₁' t s
theorem
set.left_inv_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{s : set α}
{t : set β}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β} :
set.left_inv_on f' f s → set.left_inv_on g' g t → set.maps_to f s t → set.left_inv_on (f' ∘ g') (g ∘ f) s
Right inverse
g is a right inverse to f on b if f (g x) = x for all x ∈ b.
Equations
- set.right_inv_on f' f t = set.left_inv_on f f' t
theorem
set.right_inv_on.eq_on
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{f' : β → α} :
set.right_inv_on f' f t → set.eq_on (f ∘ f') id t
theorem
set.right_inv_on.eq
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{f' : β → α}
(h : set.right_inv_on f' f t)
{y : β} :
theorem
set.right_inv_on.congr_left
{α : Type u}
{β : Type v}
{t : set β}
{f : α → β}
{f₁' f₂' : β → α} :
set.right_inv_on f₁' f t → set.eq_on f₁' f₂' t → set.right_inv_on f₂' f t
theorem
set.right_inv_on.congr_right
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f₁ f₂ : α → β}
{f' : β → α} :
set.right_inv_on f' f₁ t → set.maps_to f' t s → set.eq_on f₁ f₂ s → set.right_inv_on f' f₂ t
theorem
set.right_inv_on.surj_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α} :
set.right_inv_on f' f t → set.maps_to f' t s → set.surj_on f s t
theorem
set.right_inv_on.comp
{α : Type u}
{β : Type v}
{γ : Type w}
{t : set β}
{p : set γ}
{f : α → β}
{g : β → γ}
{f' : β → α}
{g' : γ → β} :
set.right_inv_on f' f t → set.right_inv_on g' g p → set.maps_to g' p t → set.right_inv_on (f' ∘ g') (g ∘ f) p
theorem
set.inj_on.right_inv_on_of_left_inv_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α} :
set.inj_on f s → set.left_inv_on f f' t → set.maps_to f s t → set.maps_to f' t s → set.right_inv_on f 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₂' : β → α} :
set.left_inv_on f₁' f s → set.right_inv_on f₂' f t → 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' : β → α} :
set.surj_on f s t → set.right_inv_on f f' s → set.left_inv_on f f' t
Two-side inverses
g is an inverse to f viewed as a map from a to b
Equations
- set.inv_on g f s t = (set.left_inv_on g f s ∧ set.right_inv_on g f t)
theorem
set.inv_on.symm
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α} :
set.inv_on f' f s t → set.inv_on f f' t s
theorem
set.inv_on.bij_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
{f' : β → α} :
set.inv_on f' f s t → set.maps_to f s t → set.maps_to f' t s → set.bij_on f s t
inv_fun_on is a left/right inverse
theorem
set.inj_on.left_inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
[nonempty α] :
set.inj_on f s → set.left_inv_on (function.inv_fun_on f s) f s
theorem
set.surj_on.right_inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α] :
set.surj_on f s t → set.right_inv_on (function.inv_fun_on f s) f t
theorem
set.bij_on.inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α] :
set.bij_on f s t → set.inv_on (function.inv_fun_on f s) f s t
theorem
set.surj_on.inv_on_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α] :
set.surj_on f s t → set.inv_on (function.inv_fun_on f s) f (function.inv_fun_on f s '' t) t
theorem
set.surj_on.maps_to_inv_fun_on
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α] :
set.surj_on f s t → set.maps_to (function.inv_fun_on f s) t s
theorem
set.surj_on.bij_on_subset
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
[nonempty α] :
set.surj_on f s t → set.bij_on f (function.inv_fun_on f s '' t) t
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
@[simp]
theorem
set.piecewise_insert_self
{α : Type u}
{δ : α → Sort y}
(s : set α)
(f g : Π (i : α), δ i)
{j : α}
[Π (i : α), decidable (i ∈ has_insert.insert j s)] :
(has_insert.insert j s).piecewise f g j = f j
theorem
set.piecewise_insert
{α : Type u}
{δ : α → Sort y}
(s : set α)
(f g : Π (i : α), δ i)
[Π (j : α), decidable (j ∈ s)]
[decidable_eq α]
(j : α)
[Π (i : α), decidable (i ∈ has_insert.insert j s)] :
(has_insert.insert j s).piecewise f g = function.update (s.piecewise f g) j (f j)
@[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 ∈ has_insert.insert j s)] :
(has_insert.insert j s).piecewise f g i = s.piecewise f g i
theorem
function.injective.inj_on
{α : Type u}
{β : Type v}
{f : α → β}
(h : function.injective f)
(s : set α) :
set.inj_on f s
theorem
function.injective.comp_inj_on
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
{g : β → γ}
{s : set α} :
function.injective g → set.inj_on f s → set.inj_on (g ∘ f) s
theorem
function.surjective.surj_on
{α : Type u}
{β : Type v}
{f : α → β}
(hf : function.surjective f)
(s : set β) :
set.surj_on f set.univ s
theorem
function.semiconj.maps_to_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s t : set α} :
function.semiconj f fa fb → set.maps_to fa s t → set.maps_to fb (f '' s) (f '' t)
theorem
function.semiconj.maps_to_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β} :
function.semiconj f fa fb → set.maps_to fb (set.range f) (set.range f)
theorem
function.semiconj.surj_on_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s t : set α} :
function.semiconj f fa fb → set.surj_on fa s t → set.surj_on fb (f '' s) (f '' t)
theorem
function.semiconj.surj_on_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β} :
function.semiconj f fa fb → function.surjective fa → set.surj_on fb (set.range f) (set.range f)
theorem
function.semiconj.inj_on_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s : set α} :
function.semiconj f fa fb → set.inj_on fa s → set.inj_on f (fa '' s) → set.inj_on fb (f '' s)
theorem
function.semiconj.inj_on_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β} :
function.semiconj f fa fb → function.injective fa → set.inj_on f (set.range fa) → set.inj_on fb (set.range f)
theorem
function.semiconj.bij_on_image
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
{s t : set α} :
function.semiconj f fa fb → set.bij_on fa s t → set.inj_on f t → set.bij_on fb (f '' s) (f '' t)
theorem
function.semiconj.bij_on_range
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β} :
function.semiconj f fa fb → function.bijective fa → function.injective f → set.bij_on fb (set.range f) (set.range f)
theorem
function.semiconj.maps_to_preimage
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
{s t : set β} :
set.maps_to fb s t → set.maps_to fa (f ⁻¹' s) (f ⁻¹' t)
theorem
function.semiconj.inj_on_preimage
{α : Type u}
{β : Type v}
{fa : α → α}
{fb : β → β}
{f : α → β}
(h : function.semiconj f fa fb)
{s : set β} :
set.inj_on fb s → set.inj_on f (f ⁻¹' s) → set.inj_on fa (f ⁻¹' s)
theorem
function.update_comp_eq_of_not_mem_range
{α : Type u}
{β : Type v}
{γ : Type w}
[decidable_eq β]
(g : β → γ)
{f : α → β}
{i : β}
(a : γ) :
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