Commit 2023-01-17 08:44 37a31596

View on Github →

feat: port Data.Finset.NAry (#1610)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/NAry.lean

added theorem Finset.Nonempty.image₂

added theorem Finset.Nonempty.of_image₂_left

added theorem Finset.Nonempty.of_image₂_right

added theorem Finset.bunionᵢ_image_left

added theorem Finset.bunionᵢ_image_right

added theorem Finset.card_image₂

added theorem Finset.card_image₂_iff

added theorem Finset.card_image₂_le

added theorem Finset.card_image₂_singleton_left

added theorem Finset.card_image₂_singleton_right

added theorem Finset.card_le_card_image₂_left

added theorem Finset.card_le_card_image₂_right

added theorem Finset.coe_image₂

added theorem Finset.forall_image₂_iff

added theorem Finset.image_image₂

added theorem Finset.image_image₂_antidistrib

added theorem Finset.image_image₂_antidistrib_left

added theorem Finset.image_image₂_antidistrib_right

added theorem Finset.image_image₂_distrib

added theorem Finset.image_image₂_distrib_left

added theorem Finset.image_image₂_distrib_right

added theorem Finset.image_image₂_right_anticomm

added theorem Finset.image_image₂_right_comm

added theorem Finset.image_subset_image₂_left

added theorem Finset.image_subset_image₂_right

added theorem Finset.image_uncurry_product

added def Finset.image₂

added theorem Finset.image₂_assoc

added theorem Finset.image₂_comm

added theorem Finset.image₂_congr'

added theorem Finset.image₂_congr

added theorem Finset.image₂_curry

added theorem Finset.image₂_distrib_subset_left

added theorem Finset.image₂_distrib_subset_right

added theorem Finset.image₂_empty_left

added theorem Finset.image₂_empty_right

added theorem Finset.image₂_eq_empty_iff

added theorem Finset.image₂_image_left

added theorem Finset.image₂_image_left_anticomm

added theorem Finset.image₂_image_left_comm

added theorem Finset.image₂_image_right

added theorem Finset.image₂_inter_left

added theorem Finset.image₂_inter_right

added theorem Finset.image₂_inter_singleton

added theorem Finset.image₂_inter_subset_left

added theorem Finset.image₂_inter_subset_right

added theorem Finset.image₂_left

added theorem Finset.image₂_left_comm

added theorem Finset.image₂_mk_eq_product

added theorem Finset.image₂_nonempty_iff

added theorem Finset.image₂_right

added theorem Finset.image₂_right_comm

added theorem Finset.image₂_singleton

added theorem Finset.image₂_singleton_inter

added theorem Finset.image₂_singleton_left'

added theorem Finset.image₂_singleton_left

added theorem Finset.image₂_singleton_right

added theorem Finset.image₂_subset

added theorem Finset.image₂_subset_iff

added theorem Finset.image₂_subset_left

added theorem Finset.image₂_subset_right

added theorem Finset.image₂_swap

added theorem Finset.image₂_union_left

added theorem Finset.image₂_union_right

added theorem Finset.mem_image₂

added theorem Finset.mem_image₂_iff

added theorem Finset.mem_image₂_of_mem

added theorem Finset.subset_image₂