Entry	Value
Package Name	function-thm
Count	18
Theorems	CC_EQ_I : !f. C (C f) = f C_THM : !f x y. C f x y = f y x FUNCTION_FACTORS_LEFT : !f g. (!x y. g x = g y ==> f x = f y) <=> (?h. f = h o g) FUNCTION_FACTORS_LEFT_GEN : !p f g. (!x y. p x /\ p y /\ g x = g y ==> f x = f y) <=> (?h. !x. p x ==> f x = h (g x)) FUNCTION_FACTORS_RIGHT : !f g. (!x. ?y. g y = f x) <=> (?h. f = g o h) FUNCTION_FACTORS_RIGHT_GEN : !p f g. (!x. p x ==> (?y. g y = f x)) <=> (?h. !x. p x ==> f x = g (h x)) I_O : !f. I o f = f I_THM : !x. I x = x K_THM : !x y. K x y = x O_I : !f. f o I = f SKX_EQ_I : !x. S K x = I SURJECTIVE_EXISTS_THM : !f. (!y. ?x. f x = y) <=> (!p. (?x. p (f x)) <=> (?y. p y)) SURJECTIVE_FORALL_THM : !f. (!y. ?x. f x = y) <=> (!p. (!x. p (f x)) <=> (!y. p y)) S_THM : !f g x. S f g x = f x (g x) W_THM : !f x. W f x = f x x o_ASSOC : !f g h. f o g o h = (f o g) o h o_ASSOC' : !f g h. (f o g) o h = f o g o h o_THM : !f g x. (f o g) x = f (g x)

Back to main package page