Entry	Value
Package Name	list-map-thm
Count	15
Theorems	ALL_MAP : !p f l. ALL p (MAP f l) <=> ALL (p o f) l EX_MAP : !p f l. EX p (MAP f l) <=> EX (p o f) l INJECTIVE_MAP : !f. (!l1 l2. MAP f l1 = MAP f l2 ==> l1 = l2) <=> (!x y. f x = f y ==> x = y) LENGTH_MAP : !f l. LENGTH (MAP f l) = LENGTH l MAP_APPEND : !f l1 l2. MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2) MAP_EQ : !f g l. ALL (\x. f x = g x) l ==> MAP f l = MAP g l MAP_EQ_NIL : !f l. MAP f l = [] <=> l = [] MAP_I : MAP I = I MAP_ID : !l. MAP (\x. x) l = l MAP_o : !f g l. MAP (f o g) l = MAP f (MAP g l) MAP_o' : !f g. MAP f o MAP g = MAP (f o g) MEM_MAP : !f l y. MEM y (MAP f l) <=> (?x. y = f x /\ MEM x l) NULL_MAP : !f l. NULL (MAP f l) <=> NULL l SET_OF_LIST_MAP : !f l. set_of_list (MAP f l) = IMAGE f (set_of_list l) SURJECTIVE_MAP : !f. (!ys. ?xs. MAP f xs = ys) <=> (!y. ?x. f x = y)

Back to main package page