Functions over sets #
Main definitions #
Predicate #
Set.EqOn f₁ f₂ s
: functionsf₁
andf₂
are equal at every point ofs
;Set.MapsTo f s t
:f
sends every point ofs
to a point oft
;Set.InjOn f s
: restriction off
tos
is injective;Set.SurjOn f s t
: every point ins
has a preimage ins
;Set.BijOn f s t
:f
is a bijection betweens
andt
;Set.LeftInvOn f' f s
: for everyx ∈ s
we havef' (f x) = x
;Set.RightInvOn f' f t
: for everyy ∈ t
we havef (f' y) = y
;Set.InvOn f' f s t
:f'
is a two-side inverse off
ons
andt
, i.e. we haveSet.LeftInvOn f' f s
andSet.RightInvOn f' f t
.
Functions #
Set.restrict f s
: restrict the domain off
to the sets
;Set.codRestrict f s h
: givenh : ∀ x, f x ∈ s
, restrict the codomain off
to the sets
;Set.MapsTo.restrict f s t h
: givenh : MapsTo 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 s f x = f ↑x
Instances For
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.codRestrict f s h x = { val := f x, property := h x }
Instances For
Alias of the reverse direction of Set.injective_codRestrict
.
Equality on a set #
Congruence lemmas #
Mono lemmas #
maps to #
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.MapsTo.restrict f s t h = Subtype.map f h
Instances For
Restricting the domain and then the codomain is the same as MapsTo.restrict
.
Reverse of Set.codRestrict_restrict
.
Restriction onto preimage #
The restriction of a function onto the preimage of a set.
Equations
- Set.restrictPreimage t f = Set.MapsTo.restrict f (f ⁻¹' t) t (_ : Set.MapsTo f (f ⁻¹' t) t)
Instances For
Alias of Set.restrictPreimage_injective
.
Alias of Set.restrictPreimage_surjective
.
Alias of Set.restrictPreimage_bijective
.
Injectivity on a set #
Alias of Set.injOn_of_injective
.
Alias of the forward direction of Set.injOn_iff_injective
.
Surjectivity on a set #
Bijectivity #
Alias of the forward direction of Set.bijective_iff_bijOn_univ
.
left inverse #
g
is a left inverse to f
on a
means that g (f x) = x
for all x ∈ a
.
Equations
- Set.LeftInvOn f' f s = ∀ ⦃x : α⦄, x ∈ s → f' (f x) = x
Instances For
Right inverse #
g
is a right inverse to f
on b
if f (g x) = x
for all x ∈ b
.
Equations
- Set.RightInvOn f' f t = Set.LeftInvOn f f' t
Instances For
Two-side inverses #
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 mapsTo
arguments can be deduced from
surjOn
statements using LeftInvOn.mapsTo
and RightInvOn.mapsTo
.
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
- Function.invFunOn f s b = if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst
Instances For
Monotone #
Piecewise defined function #
Alias of the forward direction of strictMono_restrict
.
Alias of the reverse direction of strictMono_restrict
.
Non-dependent version of Function.update_comp_eq_of_not_mem_range'
Equivalences, permutations #
Alias of the reverse direction of Equiv.bijOn_symm
.
Alias of the forward direction of Equiv.bijOn_symm
.