Theory "transfer"

Signature

Definitions

FUN_REL_def

⊢ ∀AB CD f g. (AB |==> CD) f g ⇔ ∀a b. AB a b ⇒ CD (f a) (g b)

PAIR_REL_def

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

bi_unique_def

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

bitotal_def

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

equalityp_def

⊢ ∀A. equalityp A ⇔ (A = $=)

left_unique_def

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

right_unique_def

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

surj_def

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

total_def

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

Theorems

ALL_IFF

⊢ bitotal AB ⇒ ((AB |==> $<=>) |==> $<=>) $! $!

ALL_surj_RDOM

⊢ surj AB ⇒ ((AB |==> $<=>) |==> $<=>) (RES_FORALL (RDOM AB)) $!

ALL_surj_iff_imp

⊢ surj AB ⇒ ((AB |==> $<=>) |==> $==>) $! $!

ALL_surj_imp_imp

⊢ surj AB ⇒ ((AB |==> $==>) |==> $==>) $! $!

ALL_total_RRANGE

⊢ total AB ⇒ ((AB |==> $<=>) |==> $<=>) $! (RES_FORALL (RRANGE AB))

ALL_total_cimp_cimp

⊢ total AB ⇒ ((AB |==> flip $==>) |==> flip $==>) $! $!

ALL_total_iff_cimp

⊢ total AB ⇒ ((AB |==> $<=>) |==> flip $==>) $! $!

COMMA_CORRECT

⊢ (AB |==> CD |==> AB ### CD) $, $,

EQ_bi_unique

⊢ bi_unique AB ⇒ (AB |==> AB |==> $<=>) $= $=

EXISTS_IFF_RDOM

⊢ surj AB ⇒ ((AB |==> $<=>) |==> $<=>) (RES_EXISTS (RDOM AB)) $?

EXISTS_IFF_RRANGE

⊢ total AB ⇒ ((AB |==> $<=>) |==> $<=>) $? (RES_EXISTS (RRANGE AB))

EXISTS_bitotal

⊢ bitotal AB ⇒ ((AB |==> $<=>) |==> $<=>) $? $?

EXISTS_surj_cimp_cimp

⊢ surj AB ⇒ ((AB |==> flip $==>) |==> flip $==>) $? $?

EXISTS_surj_iff_cimp

⊢ surj AB ⇒ ((AB |==> $<=>) |==> flip $==>) $? $?

EXISTS_total_iff_imp

⊢ total AB ⇒ ((AB |==> $<=>) |==> $==>) $? $?

EXISTS_total_imp_imp

⊢ total AB ⇒ ((AB |==> $==>) |==> $==>) $? $?

FST_CORRECT

⊢ (AB ### CD |==> AB) FST FST

FUN_REL_COMB

⊢ (AB |==> CD) f g ∧ AB a b ⇒ CD (f a) (g b)

FUN_REL_EQ2

⊢ $= |==> $= = $=

FUN_REL_IFF_IMP

⊢ (AB |==> $<=>) P Q ⇒ (AB |==> $==>) P Q ∧ (AB |==> flip $==>) P Q

LIST_REL_right_unique

⊢ right_unique AB ⇒ right_unique (LIST_REL AB)

LIST_REL_surj

⊢ surj AB ⇒ surj (LIST_REL AB)

LIST_REL_total

⊢ total AB ⇒ total (LIST_REL AB)

PAIRU_COMMA

⊢ (AB |==> $= |==> PAIRU AB) $, K

PAIRU_def

⊢ PAIRU AB (a,()) b = AB a b

PAIRU_ind

⊢ ∀P. (∀AB a b. P AB (a,()) b) ⇒ ∀v v1 v2 v3. P v (v1,v2) v3

RDOM_EQ

⊢ RDOM $= = K T

RRANGE_EQ

⊢ RRANGE $= = K T

SND_CORRECT

⊢ (AB ### CD |==> CD) SND SND

UPAIR_COMMA

⊢ ($= |==> AB |==> UPAIR AB) $, (K I)

UPAIR_def

⊢ UPAIR AB ((),a) b = AB a b

UPAIR_ind

⊢ ∀P. (∀AB a b. P AB ((),a) b) ⇒ ∀v v1 v2 v3. P v (v1,v2) v3

UREL_EQ

⊢ () = ()

bi_unique_EQ

⊢ bi_unique $=

bi_unique_implied

⊢ left_unique r ∧ right_unique r ⇒ bi_unique r

bitotal_EQ

⊢ bitotal $=

bitotal_implied

⊢ total r ∧ surj r ⇒ bitotal r

cimp_disj

⊢ (flip $==> |==> flip $==> |==> flip $==>) $\/ $\/

cimp_imp

⊢ ($==> |==> flip $==> |==> flip $==>) $==> $==>

eq_equalityp

⊢ equalityp $=

eq_imp

⊢ ($<=> |==> $<=> |==> $<=>) $==> $==>

equalityp_FUN_REL

⊢ equalityp AB ∧ equalityp CD ⇒ equalityp (AB |==> CD)

equalityp_LIST_REL

⊢ equalityp AB ⇒ equalityp (LIST_REL AB)

equalityp_PAIR_REL

⊢ equalityp AB ∧ equalityp CD ⇒ equalityp (AB ### CD)

equalityp_applied

⊢ equalityp A ⇒ A x x

imp_conj

⊢ ($==> |==> $==> |==> $==>) $/\ $/\

imp_disj

⊢ ($==> |==> $==> |==> $==>) $\/ $\/

left_unique_EQ

⊢ left_unique $=

right_unique_EQ

⊢ right_unique $=

surj_EQ

⊢ surj $=

surj_sets

⊢ surj AB ∧ right_unique AB ⇒ surj (AB |==> $<=>)

total_EQ

⊢ total $=

total_total_sets

⊢ total AB ∧ left_unique AB ⇒ total (AB |==> $<=>)