Theory "transfer"

Parents     indexedLists   patternMatches

Signature

Constant Type
FUN_REL :(α -> β -> bool) -> (γ -> δ -> bool) -> (α -> γ) -> (β -> δ) -> bool
PAIR_REL :(α -> β -> bool) -> (γ -> δ -> bool) -> α # γ -> β # δ -> bool
bi_unique :(α -> β -> bool) -> bool
bitotal :(α -> β -> bool) -> bool
left_unique :(α -> β -> bool) -> bool
right_unique :(α -> β -> bool) -> bool
surj :(α -> β -> bool) -> bool
total :(α -> β -> bool) -> bool

Definitions

total_def 
⊢ ∀R. total R ⇔ ∀x. ∃y. R x y
surj_def 
⊢ ∀R. surj R ⇔ ∀y. ∃x. R x y
right_unique_def 
⊢ ∀R. right_unique R ⇔ ∀a b1 b2. R a b1 ∧ R a b2 ⇒ (b1 = b2)
PAIR_REL_def 
⊢ ∀AB CD a c b d. (AB ### CD) (a,c) (b,d) ⇔ AB a b ∧ CD c d
left_unique_def 
⊢ ∀R. left_unique R ⇔ ∀a1 a2 b. R a1 b ∧ R a2 b ⇒ (a1 = a2)
FUN_REL_def 
⊢ ∀AB CD f g. (AB ===> CD) f g ⇔ ∀a b. AB a b ⇒ CD (f a) (g b)
bitotal_def 
⊢ ∀R. bitotal R ⇔ total R ∧ surj R
bi_unique_def 
⊢ ∀R. bi_unique R ⇔ left_unique R ∧ right_unique R

Theorems

FUN_REL_EQ2 
⊢ $= ===> $= = $=
FUN_REL_COMB 
⊢ (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)) ⇒ (AB ===> CD) (λa. f a) (λb. g b)