Functions over sets #
Main definitions #
Predicate #
set.eq_on f₁ f₂ s
: functionsf₁
andf₂
are equal at every point ofs
;set.maps_to f s t
:f
sends every point ofs
to a point oft
;set.inj_on f s
: restriction off
tos
is injective;set.surj_on f s t
: every point ins
has a preimage ins
;set.bij_on f s t
:f
is a bijection betweens
andt
;set.left_inv_on f' f s
: for everyx ∈ s
we havef' (f x) = x
;set.right_inv_on f' f t
: for everyy ∈ t
we havef (f' y) = y
;set.inv_on f' f s t
:f'
is a two-side inverse off
ons
andt
, i.e. we haveset.left_inv_on f' f s
andset.right_inv_on f' f t
.
Functions #
set.restrict f s
: restrict the domain off
to the sets
;set.cod_restrict f s h
: givenh : ∀ x, f x ∈ s
, restrict the codomain off
to the sets
;set.maps_to.restrict f s t h
: givenh : maps_to f s t
, restrict the domain off
tos
and 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
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, _⟩
Alias of injective_cod_restrict
.
Equality on a set #
Congruence lemmas #
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
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
Injectivity on a set #
f
is injective on a
if the restriction of f
to a
is injective.
Alias of inj_on_of_injective
.
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)
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)
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
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
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)
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 #
Monotone #
Piecewise defined function #
Equations
Non-dependent version of function.update_comp_eq_of_not_mem_range'