Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-19 16:05 a90f9692

View on Github →

feat(data/finset/slice): More finset.slice and antichain lemmas (#11397) Also move finset.coe_bUnion to a more sensible location.

Estimated changes

added theorem finset.coe_bUnion
added theorem finset.bUnion_slice
added theorem finset.sum_card_slice
added theorem set.sized.univ_mem_iff
added theorem set.sized_Union
added theorem set.sized_Union₂
added theorem set.sized_powerset_len
deleted theorem finset.coe_bUnion
added theorem is_antichain.least_iff
added theorem is_antichain_singleton
added theorem is_least.antichain_iff
added theorem bot_mem_lower_bounds
added theorem is_greatest_top_iff
added theorem is_least_bot_iff
added theorem top_mem_upper_bounds