Project

Namespaces

Public Vars

latte-sets.pfun

Partial functions are defined in this namespace as relations (in the type theoretic sense) of type (==> T U :type) together with a domain dom of type (set T) and a codomain cod of type (set U) such that for any element of the domain there is a unique image in the codomain.

Remark: in type theory, it is best to rely on total functions because these are ‘native’ through the function type ==>. Partial functions are encoded and thus more complex and less ‘natural’, however there are needed for many related (and set-theoretic) concepts (e.g. finite sets).

bijection

(bijection [f (rel T U)] [s1 (set T)] [s2 (set U)])
(and* (functional f s1 s2) (serial f s1 s2) (bijective f s1 s2))

Definition: The relation f is a bijection between sets s1 and s2.

bijection-injective

(bijection-injective [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(injective f s1 s2)

Theorem:

bijection-inverse-bijection

(bijection-inverse-bijection [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(bijection (ra/rinverse f) s2 s1)

Theorem: The inverse of a bijection is a bijection.

bijection-inverse-bijective

(bijection-inverse-bijective [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(bijective (ra/rinverse f) s2 s1)

Theorem: The inverse of bijective relation f is bijective.

bijection-inverse-functional

(bijection-inverse-functional [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(functional (ra/rinverse f) s2 s1)

Theorem:

bijection-inverse-injective

(bijection-inverse-injective [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(injective (ra/rinverse f) s2 s1)

Theorem: The inverse of bijective relation f is injective.

bijection-inverse-serial

(bijection-inverse-serial [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(serial (ra/rinverse f) s2 s1)

Theorem:

bijection-inverse-surjective

(bijection-inverse-surjective [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(surjective (ra/rinverse f) s2 s1)

Theorem: The inverse of bijective relation f is surjective.

bijection-surjective

(bijection-surjective [f (rel T U)] [s1 (set T)] [s2 (set U)] [b (bijection f s1 s2)])
(surjective f s1 s2)

Theorem:

bijection-unique

(bijection-unique [f (rel T U)] [s1 (set T)] [s2 (set U)])
(==>
 (bijection f s1 s2)
 (forall-in
  [z s2]
  (sq/unique-in
   s1
   (lambda [x T] (forall-in [w s2] (==> (f x w) (equal w z)))))))

Theorem: The relation f is a bijection between sets s1 and s2, hence it is unique.

bijective

(bijective [f (rel T U)] [s1 (set T)] [s2 (set U)])
(and (injective f s1 s2) (surjective f s1 s2))

Definition: The relation f is both injective and bijective wrt. sets s1 and s2. A bijection needs to be also functional and serial.

bijective-unique

(bijective-unique [f (rel T U)] [s1 (set T)] [s2 (set U)])
(==>
 (functional f s1 s2)
 (serial f s1 s2)
 (bijective f s1 s2)
 (forall-in
  [z s2]
  (sq/unique-in
   s1
   (lambda [x T] (forall-in [w s2] (==> (f x w) (equal w z)))))))

Theorem:

domain

(domain [f (rel T U)] [from (set T)] [to (set U)])
(set-of [x T] (and (elem x from) (sq/exists-in [y to] (f x y))))

Definition: The actual domain of relation f, taking antecedents in from. It is sometimes called the active domain of f.

fetch-functional-type

(fetch-functional-type def-env ctx t)

functional

(functional [f (rel T U)] [from (set T)] [to (set U)])
(forall-in
 [x from]
 (forall-in
  [y1 to]
  (forall-in [y2 to] (==> (f x y1) (f x y2) (equal y1 y2)))))

Definition: The relation f is functional (a.k.a. right-unique) on the domain-set from. and range set to.

functional-fun

(functional-fun [f (==> T U)])
(lambda [x T] (lambda [y U] (equal (f x) y)))

Definition: The “partial” function of a (total) type-theoretic function f on its whole domain

functional-fun-prop

(functional-fun-prop [f (==> T U)])
(forall
 [from (set T)]
 (forall [to (set U)] (functional (functional-fun f) from to)))

Theorem: A type-theoretic function f is a partial function for any domain restriction.

image

(image [f (rel T U)] [from (set T)] [to (set U)])
(set-of [y U] (and (elem y to) (exists-in [x from] (f x y))))

Definition: The image of set from through relation f. This is also sometimes called the range or codomain but image is less ambiguous (especially in type theory).

injection

(injection [f (rel T U)] [s1 (set T)] [s2 (set U)])
(and* (functional f s1 s2) (serial f s1 s2) (injective f s1 s2))

Definition:

injective

(injective [f (rel T U)] [from (set T)] [to (set U)])
(forall-in
 [x1 from]
 (forall-in
  [x2 from]
  (forall-in
   [y1 to]
   (forall-in
    [y2 to]
    (==> (f x1 y1) (f x2 y2) (equal y1 y2) (equal x1 x2))))))

Definition: The relation f is injective wrt. domain set from and range set to.

Note that this notion of injectivity is about comparing sets, not types. Here, the actual meaning is that s1 is less than s2.

Also, the relation is not constrained to be e.g. functional or serial (and in practice these are frequent although not always required assumptions.).

injective-contra

(injective-contra [f (rel T U)] [from (set T)] [to (set U)])
(==>
 (injective f from to)
 (forall-in
  [x1 from]
  (forall-in
   [x2 from]
   (forall-in
    [y1 to]
    (forall-in
     [y2 to]
     (==>
      (f x1 y1)
      (f x2 y2)
      (not (equal x1 x2))
      (not (equal y1 y2))))))))

Theorem: The contrapositive of injective, useful for proofs by contradiction.

injective-single

(injective-single [f (rel T U)] [s1 (set T)] [s2 (set U)])
(==>
 (serial f s1 s2)
 (injective f s1 s2)
 (forall-in
  [z s2]
  (sq/single-in
   s1
   (lambda [x T] (forall-in [w s2] (==> (f x w) (equal w z)))))))

Theorem:

ridentity-functional

(ridentity-functional [T :type])
(forall
 [from (set T)]
 (forall [to (set T)] (functional (rel/identity T) from to)))

Theorem: The identity relation is a partial function on any domain set.

ridentity-injective

(ridentity-injective [T :type])
(forall [s (set T)] (injective (rel/identity T) s s))

Theorem:

serial

(serial [f (rel T U)] [from (set T)] [to (set U)])
(forall-in [x from] (exists-in [y to] (f x y)))

Definition: The relation f covers all of (is total wrt.) the provided from domain set.

serial-alt

(serial-alt [f (rel T U)] [from (set T)] [to (set U)])
(seteq (domain f from to) from)

Definition: Alternative definition for serial.

serial-alt-serial

(serial-alt-serial [f (rel T U)] [from (set T)] [to (set U)])
(==> (serial-alt f from to) (serial f from to))

Theorem:

serial-serial-alt

(serial-serial-alt [f (rel T U)] [from (set T)] [to (set U)])
(==> (serial f from to) (serial-alt f from to))

Theorem:

smaller

(smaller [s1 (set T)] [s2 (set U)])
(rel-ex (lambda [f (rel T U)] (injection f s1 s2)))

Definition: The set s1 is “smaller” than s2.

surjection

(surjection [f (rel T U)] [s1 (set T)] [s2 (set U)])
(and* (functional f s1 s2) (serial f s1 s2) (surjective f s1 s2))

Definition: The relation f is a functional surjection on-to set s2.

surjective

(surjective [f (rel T U)] [s1 (set T)] [s2 (set U)])
(forall-in [y s2] (exists-in [x s1] (f x y)))

Definition: The relation f is surjective onto s2 for domain s1.