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