Commit 2022-12-13 10:38 e40deb4b

View on Github →

feat port: Data.Set.NAry (#969) cf9386b56953fb40904843af98b7a80757bbe7f9 Easy. I changed the header because it seemed wrong in Lean3.

Estimated changes

added theorem Set.Nonempty.image2
added theorem Set.forall_image2_iff
added def Set.image2
added theorem Set.image2_assoc
added theorem Set.image2_comm
added theorem Set.image2_congr'
added theorem Set.image2_congr
added theorem Set.image2_empty_left
added theorem Set.image2_empty_right
added theorem Set.image2_image2_left
added theorem Set.image2_image_left
added theorem Set.image2_image_right
added theorem Set.image2_left
added theorem Set.image2_left_comm
added theorem Set.image2_right
added theorem Set.image2_right_comm
added theorem Set.image2_singleton
added theorem Set.image2_subset
added theorem Set.image2_subset_iff
added theorem Set.image2_subset_left
added theorem Set.image2_swap
added theorem Set.image2_union_left
added theorem Set.image2_union_right
added def Set.image3
added theorem Set.image3_congr'
added theorem Set.image3_congr
added theorem Set.image3_mono
added theorem Set.image_image2
added theorem Set.mem_image2
added theorem Set.mem_image2_iff
added theorem Set.mem_image2_of_mem
added theorem Set.mem_image3