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