The Theory bin_rel

Parents

hol

Children

topology

fun_rel

Constants

$	'a 'b 'a 'b
$	'a SET 'b SET ('a 'b) SET
$	'a SET 'b SET ('a 'b) SET SET
Dom	('a 'b) SET 'a SET
Ran	('a 'b) SET 'b SET
Id	'a SET ('a 'a) SET
Graph	('a 'b) ('a 'b) SET
$⨟	('a 'b) ('b 'c) 'a 'c
$R_⨟_R	('a 'b) SET ('b 'c) SET ('a 'c) SET
$R_o_R	('b 'c) SET ('a 'b) SET ('a 'c) SET
$	'a SET ('a 'b) SET ('a 'b) SET
$▷	('a 'b) SET 'b SET ('a 'b) SET
$⩤	'a SET ('a 'b) SET ('a 'b) SET
$⩥	('a 'b) SET 'b SET ('a 'b) SET
InvRel	('a 'b) SET ('b 'a) SET
$Image	('a 'b) SET 'a SET 'b SET
Reflexive	('a 'a) SET SET
Symmetric	('a 'a) SET SET
Transitive	('a 'a) SET SET
Injective	('a 'b) SET SET
Surjective	'b SET ('a 'b) SET SET
Total	'a SET ('a 'b) SET SET
Functional	('a 'b) SET SET
$⊕	('a 'b) SET ('a 'b) SET ('a 'b) SET
$⁺	('a 'a) SET ('a 'a) SET
$^*	('a 'a) SET ('a 'a) SET
RelCombine	('a 'b) SET ('a 'c) SET ('a 'b 'c) SET

Aliases

⨟	$R_⨟_R : ('b 'a) SET ('a 'c) SET ('b 'c) SET
o	$R_o_R : ('a 'c) SET ('b 'a) SET ('b 'c) SET
^~	InvRel : ('b 'a) SET ('a 'b) SET

Type_Abbreviations

'a	'a SET
'a 'b	('a 'b) SET

Fixity

Right Infix 240:

R_o_R

R_⨟_R

⩥

▷

⊕

⨟

⩤

Right Infix 280:

Image

Right Infix 300:

Postfix 300:

⁺

Definitions

	$ = $,
	x y (x y) = {(v, w)\|v x w y}
	x y x y = (x y)
Dom	r Dom r = {x\| y (x, y) r}
Ran	r Ran r = {y\| x (x, y) r}
Id	s Id s = {(x, y)\|x = y x s}
Graph	f Graph f = {(x, y)\|y = f x}
⨟	f g f ⨟ g = g o f
R_⨟_R	r s r ⨟ s = {(x, z)\| y (x, y) r (y, z) s}
R_o_R	r s r o s = s ⨟ r
	a r a r = {(x, y)\|x a (x, y) r}
▷	a r r ▷ a = {(x, y)\|y a (x, y) r}
⩤	a r a ⩤ r = {(x, y)\| x a (x, y) r}
⩥	a r r ⩥ a = {(x, y)\| y a (x, y) r}
InvRel	r r ^~ = {(x, y)\|(y, x) r}
Image	r s r Image s = {y\| x x s (x, y) r}
Reflexive	Reflexive = {r\| x (x, x) r}
Symmetric	Symmetric = {r\| x y (x, y) r (y, x) r}
Transitive	Transitive = {r\| x y z (x, y) r (y, z) r (x, z) r}
Injective	Injective = {r\| x y z (x, z) r (y, z) r x = y}
Surjective	s Surjective s = {r\|s = Ran r}
Total	s Total s = {r\|s = Dom r}
Functional	Functional = {r\| x w z (x, w) r (x, z) r w = z}
⊕	r s r ⊕ s = (Dom s ⩤ r) s
⁺	r r ⁺ = {q\|r q q Transitive}
^*	r r ^* = {q\|r q q Reflexive q Transitive}
RelCombine	f g RelCombine f g = {(x, y, z)\|(x, y) f (x, z) g}

Theorems

rel__in_clauses	a b x x1 y z r r1 r2 s t q f (x y r (x, y) r) ((x, y) (a b) x a y b) (r a b r (a b)) (x Dom r ( y (x, y) r)) (y Ran r ( x (x, y) r)) ((x, x1) Id a x = x1 x a) ((x, y) Graph f y = f x) ((x, z) r ⨟ s ( y (x, y) r (y, z) s)) ((x, z) s o r (x, z) r ⨟ s) ((x, y) a r x a (x, y) r) ((x, y) r ▷ b y b (x, y) r) ((x, y) a ⩤ r x a (x, y) r) ((x, y) r ⩥ b y b (x, y) r) ((y, x) r ^~ (x, y) r) (y r Image a ( x x a (x, y) r)) (q Reflexive ( x (x, x) q)) (q Symmetric ( x1 x2 (x1, x2) q (x2, x1) q)) (q Transitive ( x1 x2 x3 (x1, x2) q (x2, x3) q (x1, x3) q)) (r Injective ( x1 x2 y (x1, y) r (x2, y) r x1 = x2)) (r Surjective b ( y y b ( x (x, y) r))) (r Total a ( x x a ( y (x, y) r))) (r Functional ( x y1 y2 (x, y1) r (x, y2) r y1 = y2)) ((x, y) r1 ⊕ r2 (x, y) (Dom r2 ⩤ r1) r2) ((x, y, z) RelCombine r t (x, y) r (x, z) t)
bin_rel_ext_clauses	r1 r2 (r1 r2 ( x y (x, y) r1 (x, y) r2) ( x y (x, y) r1 (x, y) r2)) (r1 r2 ( x y (x, y) r1 (x, y) r2)) (r1 = r2 ( x y (x, y) r1 (x, y) r2))
inv_rel_thm	f a b (f ^~ Functional f Injective) (f ^~ Injective f Functional) (f ^~ Surjective a f Total a) (f ^~ Total b f Surjective b)
bin_rel__universe_thm	f g r0 r1 a b (Dom r0 = {} r0 = {}) (Ran r0 = {} r0 = {}) Dom {} = {} Ran {} = {} Dom Universe = Universe Ran Universe = Universe (Id r0 = {} r0 = {}) Id {} = {} (r0 ^~ = {} r0 = {}) {} ^~ = {} Universe ^~ = Universe r0 ⨟ {} = {} {} ⨟ r0 = {} ({} = r0 ⨟ r1 Ran r0 Dom r1 = {}) (r0 ⨟ r1 = {} Ran r0 Dom r1 = {}) RelCombine r0 {} = {} RelCombine {} r0 = {} r0 Image {} = {} {} Image a = {} f ⊕ {} = f {} ⊕ f = f (f ⊕ g = {} f = {} g = {}) (f = {} g = {} f ⊕ g = {}) (f ⊕ g = {} f = {} g = {}) f ⊕ Universe = Universe Universe ⩤ r0 = {} a ⩤ {} = {} {} ⩤ r0 = r0 Universe r0 = r0 a {} = {} {} r0 = {} r0 ⩥ Universe = {} {} ⩥ b = {} r0 ⩥ {} = r0 r0 ▷ Universe = r0 {} ▷ b = {} r0 ▷ {} = {}
bin_rel_insert_thm	a b r x xy y Dom (Insert (x, y) r) = Insert x (Dom r) Dom (Insert xy r) = Insert (Fst xy) (Dom r) Ran (Insert (x, y) r) = Insert y (Ran r) Ran (Insert xy r) = Insert (Snd xy) (Ran r) Id (Insert x a) = Insert (x, x) (Id a) Insert (x, y) r Image a = r Image a (if x a then {y} else {}) Insert (x, y) r ⩥ b = (r ⩥ b) (if y b then {(x, y)} else {}) Insert (x, y) r ▷ b = (r ▷ b) (if y b then {(x, y)} else {}) a ⩤ Insert (x, y) r = (a ⩤ r) (if x a then {(x, y)} else {}) a Insert (x, y) r = (a r) (if x a then {(x, y)} else {}) Insert (x, y) r ^~ = Insert (y, x) (r ^~)