Project

Namespaces

Public Vars

latte-sets.equiv

Equivalence relations

all-disjoint

(all-disjoint [P (powerset T)])
(forall
 [s1 s2 (set T)]
 (==>
  (set-elem s1 P)
  (set-elem s2 P)
  (not (set-equal s1 s2))
  (set-equal (inter s1 s2) (emptyset T))))

Definition: The sets of partition P are all disjoints

all-nonempty

(all-nonempty [P (powerset T)])
(forall
 [s (set T)]
 (==> (set-elem s P) (not (set-equal s (emptyset T)))))

Definition:

eqclass

(eqclass [x T] [R (rel T T)] [eqR (equivalence R)])
(lambda [y T] (R x y))

Definition: The equivalence class of element x wrt. relation R.

eqclass-eq

(eqclass-eq [x T] [y T] [R (rel T T)] [eqR (equivalence R)])
(==> (R x y) (seteq (eqclass x R eqR) (eqclass y R eqR)))

Theorem:

eqclass-equal

(eqclass-equal [x T] [y T] [R (rel T T)] [eqR (equivalence R)])
(==> (R x y) (set-equal (eqclass x R eqR) (eqclass y R eqR)))

Theorem:

eqclass-mem

(eqclass-mem [x T] [R (rel T T)] [eqR (equivalence R)])
(elem x (eqclass x R eqR))

Theorem:

eqclass-subset

(eqclass-subset [x T] [y T] [R (rel T T)] [eqR (equivalence R)])
(==> (R x y) (subset (eqclass x R eqR) (eqclass y R eqR)))

Theorem:

equiv-refl

(equiv-refl [R (rel T T)] [eqR (equivalence R)])
(reflexive R)

Theorem:

equiv-sym

(equiv-sym [R (rel T T)] [eqR (equivalence R)])
(symmetric R)

Theorem:

equiv-trans

(equiv-trans [R (rel T T)] [eqR (equivalence R)])
(transitive R)

Theorem:

equivalence

(equivalence [R (rel T T)])
(and* (reflexive R) (symmetric R) (transitive R))

Definition: An equivalence relation.

ident-equiv

(ident-equiv [T :type])
(equivalence (rel/identity T))

Theorem: The indentity on T is an equivalence relation.

partition

(partition [S (set T)] [P (powerset T)])
(and* (all-nonempty P) (partition-member S P) (all-disjoint P))

Definition: P is a partition of set s

partition-member

(partition-member [s (set T)] [P (powerset T)])
(forall-in
 [x s]
 (set-ex (lambda [sp (set T)] (and (set-elem sp P) (elem x sp)))))

Definition: The elements of set s are members of partition P