Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-04 14:28 f55d3524

View on Github →

feat(order/filter/n_ary): Binary and ternary maps of filters (#13062) Define filter.map₂ and filter.map₃, the binary and ternary maps of filters.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.image_subset_image2_left

added theorem set.image_subset_image2_right

Created src/order/filter/n_ary.lean

added theorem filter.image2_mem_map₂

added theorem filter.le_map₂_iff

added theorem filter.map_map₂

added theorem filter.map_map₂_antidistrib

added theorem filter.map_map₂_antidistrib_left

added theorem filter.map_map₂_antidistrib_right

added theorem filter.map_map₂_distrib

added theorem filter.map_map₂_distrib_left

added theorem filter.map_map₂_distrib_right

added theorem filter.map_map₂_right_anticomm

added theorem filter.map_map₂_right_comm

added def filter.map₂

added theorem filter.map₂_assoc

added theorem filter.map₂_bot_left

added theorem filter.map₂_bot_right

added theorem filter.map₂_comm

added theorem filter.map₂_eq_bot_iff

added theorem filter.map₂_inf_subset_left

added theorem filter.map₂_inf_subset_right

added theorem filter.map₂_left

added theorem filter.map₂_left_comm

added theorem filter.map₂_map_left

added theorem filter.map₂_map_left_anticomm

added theorem filter.map₂_map_left_comm

added theorem filter.map₂_map_right

added theorem filter.map₂_map₂_left

added theorem filter.map₂_map₂_right

added theorem filter.map₂_mono

added theorem filter.map₂_mono_left

added theorem filter.map₂_mono_right

added theorem filter.map₂_ne_bot_iff

added theorem filter.map₂_pure

added theorem filter.map₂_pure_left

added theorem filter.map₂_pure_right

added theorem filter.map₂_right

added theorem filter.map₂_right_comm

added theorem filter.map₂_sup_left

added theorem filter.map₂_sup_right

added theorem filter.map₂_swap

added def filter.map₃

added theorem filter.mem_map₂_iff

added theorem filter.ne_bot.map₂