Theory "transfer"

Signature

Definitions

right_unique_def

⊢ ∀R. right_unique R ⇔ ∀a b1 b2. R a b1 ∧ R a b2 ⇒ b1 = b2

left_unique_def

⊢ ∀R. left_unique R ⇔ ∀a1 a2 b. R a1 b ∧ R a2 b ⇒ a1 = a2

bi_unique_def

⊢ ∀R. bi_unique R ⇔ left_unique R ∧ right_unique R

total_def

⊢ ∀R. total R ⇔ ∀x. ∃y. R x y

surj_def

⊢ ∀R. surj R ⇔ ∀y. ∃x. R x y

bitotal_def

⊢ ∀R. bitotal R ⇔ total R ∧ surj R

FUN_REL_def

⊢ ∀AB CD f g. FUN_REL AB CD f g ⇔ ∀a b. AB a b ⇒ CD (f a) (g b)

PAIR_REL_def

⊢ ∀AB CD a c b d. PAIR_REL AB CD (a,c) (b,d) ⇔ AB a b ∧ CD c d

Theorems

FUN_REL_COMB

⊢ FUN_REL AB CD f g ∧ AB a b ⇒ CD (f a) (g b)

FUN_REL_ABS

⊢ (∀a b. AB a b ⇒ CD (f a) (g b)) ⇒ FUN_REL AB CD (λa. f a) (λb. g b)

FUN_REL_EQ2

⊢ FUN_REL $= $= = $=