Entry Value
Package Name pair-thm
Count 20
Theorems
  • CHOICE_PAIRED_THM : !p q. (?a b. p a b) /\ (!a b. p a b ==> q (a,b)) ==> q (@(a,b). p a b)
  • CHOICE_UNPAIR_THM : !p. (@(a,b). p a b) = (@x. p (FST x) (SND x))
  • EXISTS_CURRY : !p. (?f. p f) <=> (?f. p (\(a,b). f a b))
  • EXISTS_PAIRED_THM : !p. (?(a,b). p a b) <=> (?a b. p a b)
  • EXISTS_PAIR_THM : !p. (?x. p x) <=> (?a b. p (a,b))
  • EXISTS_TRIPLED_THM : !p. (?(a,b,c). p a b c) <=> (?a b c. p a b c)
  • EXISTS_UNCURRY : !p. (?f. p f) <=> (?f. p (\a b. f (a,b)))
  • EXISTS_UNPAIR_THM : !p. (?x y. p x y) <=> (?z. p (FST z) (SND z))
  • FORALL_CURRY : !p. (!f. p f) <=> (!f. p (\(a,b). f a b))
  • FORALL_PAIRED_THM : !p. (!(a,b). p a b) <=> (!a b. p a b)
  • FORALL_PAIR_THM : !p. (!x. p x) <=> (!a b. p (a,b))
  • FORALL_TRIPLED_THM : !p. (!(a,b,c). p a b c) <=> (!a b c. p a b c)
  • FORALL_UNCURRY : !p. (!f. p f) <=> (!f. p (\a b. f (a,b)))
  • FORALL_UNPAIR_THM : !p. (!x y. p x y) <=> (!z. p (FST z) (SND z))
  • LAMBDA_PAIR_THM : !f. (\x. f x) = (\(a,b). f (a,b))
  • LAMBDA_UNPAIR_THM : !f. (\(x,y). f x y) = (\p. f (FST p) (SND p))
  • PAIR : !x. FST x,SND x = x
  • PAIRED_ETA_THM : (!f. (\(a,b). f (a,b)) = f) /\ (!f. (\(a,b,c). f (a,b,c)) = f) /\ (!f. (\(a,b,c,d). f (a,b,c,d)) = f)
  • pair_INDUCT : !p. (!a b. p (a,b)) ==> (!x. p x)
  • pair_RECURSION : !f. ?fn. !a b. fn (a,b) = f a b
    		•
    Back to main package page