Latte-sets 1.0b10-SNAPSHOT
Released under the MIT Licence
A formalization of (typed) Set theory in LaTTe.
Installation
To install, add the following dependency to your project or build file:
[latte-sets "1.0b10-SNAPSHOT"]
Namespaces
latte-sets.algebra
The boolean algebra operators for sets.
Public variables and functions:
- comp-empty-full
- comp-full-empty
- complement
- diff
- diff-cancel
- diff-empty-left
- diff-empty-right
- dist-inter-union
- dist-inter-union-sym
- dist-union-inter
- dist-union-inter-sym
- inter
- inter-assoc
- inter-assoc-sym
- inter-commute
- inter-elim-left
- inter-elim-right
- inter-empty
- inter-idem
- symdiff
- symdiff-alt
- union
- union-assoc
- union-assoc-sym
- union-commute
- union-empty
- union-idem
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.
Public variables and functions:
- bijection
- bijection-injective
- bijection-inverse-bijection
- bijection-inverse-bijective
- bijection-inverse-functional
- bijection-inverse-injective
- bijection-inverse-serial
- bijection-inverse-surjective
- bijection-surjective
- bijection-unique
- bijective
- bijective-unique
- domain
- fetch-functional-type
- functional
- functional-fun
- functional-fun-prop
- image
- injection
- injective
- injective-contra
- injective-single
- ridentity-functional
- ridentity-injective
- serial
- serial-alt
- serial-alt-serial
- serial-serial-alt
- smaller
- surjection
- surjective
latte-sets.powerrel
Notions about the relational powerset construction.
Public variables and functions:
- fetch-powerrel-types
- powerrel
- rel-elem
- rel-ex
- rel-ex-elim
- rel-ex-intro
- rel-single
- rel-unique
- rintersections
- rintersections-lower-bound
- rintersections-prop
- runions
- runions-upper-bound
- the-rel
- the-rel-lemma
- the-rel-prop
- trans-closure
- trans-closure-set
- trans-closure-smallest
- trans-closure-sub
- transitive-trans-closure
latte-sets.powerset
Notions about the powerset construction.
Public variables and functions:
- empty-powerset
- empty-powerset-prop
- fetch-powerset-type
- full-powerset
- full-powerset-prop
- intersections
- intersections-lower-bound
- intersections-prop
- powerset
- powerset1
- powerset1-prop
- powerset1-prop-conv
- powerset1-prop-equiv
- set-elem
- set-ex
- set-ex-elim
- set-ex-intro
- set-single
- set-unique
- the-set
- the-set-lemma
- the-set-prop
- unions
- unions-upper-bound
latte-sets.quant
Quantifiers over sets (rather than types), with most definitions specialized from latte-prelude.quant.
Public variables and functions:
- decompose-exists-in-type
- decompose-forall-in-type
- decompose-single-in-type
- ex-in-elim
- ex-in-elim-rule
- ex-in-intro
- exists-in
- forall-in
- single-in
- single-in-elim
- single-in-elim-rule
- single-in-intro
- the-element
- the-element-ax
- the-element-lemma
- the-element-lemma-prop
- the-element-prop
- the-element-prop-ax
- unique-in
latte-sets.ralgebra
The relation algebra operators.
Public variables and functions:
- dist-rinter-runion
- dist-rinter-runion-sym
- dist-runion-rinter
- dist-runion-rinter-sym
- rcomp-empty-full
- rcomp-full-empty
- rcomplement
- rdiff
- rdiff-cancel
- rdiff-empty-left
- rdiff-empty-right
- restrict-dom
- restrict-dom-dom
- restrict-ran
- rimage
- rinter
- rinter-assoc
- rinter-assoc-sym
- rinter-commute
- rinter-elim-left
- rinter-elim-right
- rinter-empty
- rinter-idem
- rinverse
- rinverse-prop
- runion
- runion-assoc
- runion-assoc-sym
- runion-commute
- runion-dom
- runion-empty
- runion-idem
- runion-ran
- subtract-dom
- subtract-ran
latte-sets.rel
A relation from elements of a given type T to elements of U is formalized with type (==> T U :type).
Public variables and functions:
- dom
- emptyrel
- emptyrel-prop
- fetch-rel-type
- fullrel
- fullrel-prop
- functional
- funrel
- funrel-functional
- ident-refl
- ident-sym
- ident-trans
- identity
- prod
- psubrel
- psubrel-antirefl
- psubrel-antisym
- psubrel-emptyrel
- psubrel-emptyrel-conv
- psubrel-emptyrel-equiv
- psubrel-trans
- ran
- rcomp
- rcomp-assoc
- rcomp-assoc-subrel
- rcomp-assoc-suprel
- refl-closure
- refl-closure-smallest
- refl-closure-sub
- reflexive
- reflexive-refl-closure
- rel
- rel-equal
- rel-equal-implies-releq
- rel-equal-implies-subrel
- rel-equal-prop
- rel-equal-refl
- rel-equal-releq
- rel-equal-sym
- rel-equal-trans
- releq
- releq-implies-rel-equal
- releq-refl
- releq-sym
- releq-trans
- relfun
- relfun-img
- relfun-img-prop
- relfunrel-equal
- relfunrel-ext-equal
- subrel
- subrel-emptyrel-lower-bound
- subrel-fullrel-upper-bound
- subrel-prop
- subrel-refl
- subrel-trans
- symm-closure
- symm-closure-smallest
- symm-closure-sub
- symmetric
- symmetric-symm-closure
- transitive
latte-sets.set
Set-theoretic notions based on the subset approach of type theory.
Public variables and functions:
- elem
- elem-def
- element-type-of
- emptyset
- emptyset-prop
- fetch-set-type
- fullset
- fullset-intro
- psubset
- psubset-antirefl
- psubset-antisym
- psubset-emptyset
- psubset-emptyset-conv
- psubset-emptyset-equiv
- psubset-trans
- set
- set-equal
- set-equal-implies-seteq
- set-equal-implies-subset
- set-equal-prop
- set-equal-refl
- set-equal-seteq
- set-equal-sym
- set-equal-trans
- set-of
- seteq
- seteq-implies-set-equal
- seteq-refl
- seteq-sym
- seteq-trans
- subset
- subset-elim
- subset-emptyset-lower-bound
- subset-fullset-upper-bound
- subset-intro
- subset-prop
- subset-refl
- subset-trans