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
fill= {r|∀ x y z• (x, y) ∈ r ∧ (y, z) ∈ r ⇒ (x, z) ∈ r}
Injective
⊢ Injective
fill= {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
fill= {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
fill• r *
fill= ⋂ {q|r ⊆ q ∧ q ∈ Reflexive ∧ q ∈ Transitive}
RelCombine
⊢ ∀ f g
fill• RelCombine f g
fill= {(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
fill• (x ↦ y ∈ r ⇔ (x, y) ∈ r)
fill∧ ((x, y) ∈ (a × b) ⇔ x ∈ a ∧ y ∈ b)
fill∧ (r ∈ a ↔ b ⇔ r ⊆ (a × b))
fill∧ (x ∈ Dom r ⇔ (∃ y• (x, y) ∈ r))
fill∧ (y ∈ Ran r ⇔ (∃ x• (x, y) ∈ r))
fill∧ ((x, x1) ∈ Id a ⇔ x = x1 ∧ x ∈ a)
fill∧ ((x, y) ∈ Graph f ⇔ y = f x)
fill∧ ((x, z) ∈ r ⨟ s
fill⇔ (∃ y• (x, y) ∈ r ∧ (y, z) ∈ s))
fill∧ ((x, z) ∈ s o r ⇔ (x, z) ∈ r ⨟ s)
fill∧ ((x, y) ∈ a ⊲ r ⇔ x ∈ a ∧ (x, y) ∈ r)
fill∧ ((x, y) ∈ r ▷ b ⇔ y ∈ b ∧ (x, y) ∈ r)
fill∧ ((x, y) ∈ a ⩤ r ⇔ ¬ x ∈ a ∧ (x, y) ∈ r)
fill∧ ((x, y) ∈ r ⩥ b ⇔ ¬ y ∈ b ∧ (x, y) ∈ r)
fill∧ ((y, x) ∈ r ~ ⇔ (x, y) ∈ r)
fill∧ (y ∈ r Image a ⇔ (∃ x• x ∈ a ∧ (x, y) ∈ r))
fill∧ (q ∈ Reflexive ⇔ (∀ x• (x, x) ∈ q))
fill∧ (q ∈ Symmetric
fill⇔ (∀ x1 x2• (x1, x2) ∈ q ⇒ (x2, x1) ∈ q))
fill∧ (q ∈ Transitive
fill⇔ (∀ x1 x2 x3
fill• (x1, x2) ∈ q ∧ (x2, x3) ∈ q ⇒ (x1, x3) ∈ q))
fill∧ (r ∈ Injective
fill⇔ (∀ x1 x2 y
fill• (x1, y) ∈ r ∧ (x2, y) ∈ r ⇒ x1 = x2))
fill∧ (r ∈ Surjective b
fill⇔ (∀ y• y ∈ b ⇔ (∃ x• (x, y) ∈ r)))
fill∧ (r ∈ Total a
fill⇔ (∀ x• x ∈ a ⇔ (∃ y• (x, y) ∈ r)))
fill∧ (r ∈ Functional
fill⇔ (∀ x y1 y2
fill• (x, y1) ∈ r ∧ (x, y2) ∈ r ⇒ y1 = y2))
fill∧ ((x, y) ∈ r1 ⊕ r2
fill⇔ (x, y) ∈ (Dom r2 ⩤ r1) ∪ r2)
fill∧ ((x, y, z) ∈ RelCombine r t
fill⇔ (x, y) ∈ r ∧ (x, z) ∈ t)
bin_rel_ext_clauses
⊢ ∀ r1 r2
fill• (r1 ⊂ r2
fill⇔ (∀ x y• (x, y) ∈ r1 ⇒ (x, y) ∈ r2)
fill∧ (∃ x y• ¬ (x, y) ∈ r1 ∧ (x, y) ∈ r2))
fill∧ (r1 ⊆ r2 ⇔ (∀ x y• (x, y) ∈ r1 ⇒ (x, y) ∈ r2))
fill∧ (r1 = r2 ⇔ (∀ x y• (x, y) ∈ r1 ⇔ (x, y) ∈ r2))
inv_rel_thm
⊢ ∀ f a b
fill• (f ~ ∈ Functional ⇔ f ∈ Injective)
fill∧ (f ~ ∈ Injective ⇔ f ∈ Functional)
fill∧ (f ~ ∈ Surjective a ⇔ f ∈ Total a)
fill∧ (f ~ ∈ Total b ⇔ f ∈ Surjective b)
bin_rel_∅_universe_thm
⊢ ∀ f g r0 r1 a b
fill• (Dom r0 = {} ⇔ r0 = {})
fill∧ (Ran r0 = {} ⇔ r0 = {})
fill∧ Dom {} = {}
fill∧ Ran {} = {}
fill∧ Dom Universe = Universe
fill∧ Ran Universe = Universe
fill∧ (Id r0 = {} ⇔ r0 = {})
fill∧ Id {} = {}
fill∧ (r0 ~ = {} ⇔ r0 = {})
fill∧ {} ~ = {}
fill∧ Universe ~ = Universe
fill∧ r0 ⨟ {} = {}
fill∧ {} ⨟ r0 = {}
fill∧ ({} = r0 ⨟ r1 ⇔ Ran r0 ∩ Dom r1 = {})
fill∧ (r0 ⨟ r1 = {} ⇔ Ran r0 ∩ Dom r1 = {})
fill∧ RelCombine r0 {} = {}
fill∧ RelCombine {} r0 = {}
fill∧ r0 Image {} = {}
fill∧ {} Image a = {}
fill∧ f ⊕ {} = f
fill∧ {} ⊕ f = f
fill∧ (f ⊕ g = {} ⇔ f = {} ∧ g = {})
fill∧ (f = {} ∧ g = {} ⇒ f ⊕ g = {})
fill∧ (f ⊕ g = {} ⇔ f = {} ∧ g = {})
fill∧ f ⊕ Universe = Universe
fill∧ Universe ⩤ r0 = {}
fill∧ a ⩤ {} = {}
fill∧ {} ⩤ r0 = r0
fill∧ Universe ⊲ r0 = r0
fill∧ a ⊲ {} = {}
fill∧ {} ⊲ r0 = {}
fill∧ r0 ⩥ Universe = {}
fill∧ {} ⩥ b = {}
fill∧ r0 ⩥ {} = r0
fill∧ r0 ▷ Universe = r0
fill∧ {} ▷ b = {}
fill∧ r0 ▷ {} = {}
bin_rel_insert_thm
⊢ ∀ a b r x xy y
fill• Dom (Insert (x, y) r) = Insert x (Dom r)
fill∧ Dom (Insert xy r) = Insert (Fst xy) (Dom r)
fill∧ Ran (Insert (x, y) r) = Insert y (Ran r)
fill∧ Ran (Insert xy r) = Insert (Snd xy) (Ran r)
fill∧ Id (Insert x a) = Insert (x, x) (Id a)
fill∧ Insert (x, y) r Image a
fill= r Image a ∪ (if x ∈ a then {y} else {})
fill∧ Insert (x, y) r ⩥ b
fill= (r ⩥ b) ∪ (if ¬ y ∈ b then {(x, y)} else {})
fill∧ Insert (x, y) r ▷ b
fill= (r ▷ b) ∪ (if y ∈ b then {(x, y)} else {})
fill∧ a ⩤ Insert (x, y) r
fill= (a ⩤ r) ∪ (if ¬ x ∈ a then {(x, y)} else {})
fill∧ a ⊲ Insert (x, y) r
fill= (a ⊲ r) ∪ (if x ∈ a then {(x, y)} else {})
fill∧ Insert (x, y) r ~ = Insert (y, x) (r ~)

up quick index

privacy policy

Created:

V