Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 00:26 43514e1e

View on Github →

feat(data/option/n_ary): Binary map of options (#16763) Define option.map₂, the binary map of options.

Estimated changes

added theorem finset.image₂_def
added theorem finset.image₂_curry
added theorem option.coe_ne_none
added theorem option.some_eq_coe
added theorem option.map_map₂
added theorem option.map_uncurry
added def option.map₂
added theorem option.map₂_assoc
added theorem option.map₂_coe_coe
added theorem option.map₂_coe_left
added theorem option.map₂_comm
added theorem option.map₂_curry
added theorem option.map₂_def
added theorem option.map₂_map_left
added theorem option.map₂_swap
added theorem option.mem_map₂_iff
added theorem set.image2_def
added theorem set.image2_curry
added theorem set.image_uncurry_prod
added theorem filter.map₂_curry