The Theory bin

The Theory bin_rel

Parents

hol

Children

topology

fun_rel

Constants

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

Aliases

⨟	$R_⨟_R : 'b ↔ 'a → 'a ↔ 'c → 'b ↔ 'c
o	$R_o_R : 'a ↔ 'c → 'b ↔ 'a → 'b ↔ 'c
^~	InvRel : 'b ↔ 'a → 'a ↔ 'b

Type_Abbreviations

'a ℘	'a ℘
'a ↔ 'b	'a ↔ 'b

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 ^~)

Created: