Commit 2023-01-24 07:35 c6bb17d5

View on Github →

feat: Port order.filter.n_ary (#1786)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/NAry.lean

added theorem Filter.NeBot.map₂

added theorem Filter.NeBot.of_map₂_left

added theorem Filter.NeBot.of_map₂_right

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 theorem Filter.map_prod_eq_map₂'

added theorem Filter.map_prod_eq_map₂

added theorem Filter.map_uncurry_prod

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₂_curry

added theorem Filter.map₂_distrib_le_left

added theorem Filter.map₂_distrib_le_right

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₂_left_identity

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₂_mk_eq_prod

added theorem Filter.map₂_mono

added theorem Filter.map₂_mono_left

added theorem Filter.map₂_mono_right

added theorem Filter.map₂_neBot_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₂_right_identity

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