Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.union_sdiff_self_eq_union

Modification history

2022-09-04 15:22
src/data/finset/basic.lean
feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281) …
Modified finset.union_sdiff_self_eq_unionView on Github →
2021-12-22 23:07
src/data/finset/basic.lean
feat(data/finset/*): Random lemmas (#10955) …
Modified finset.union_sdiff_self_eq_unionView on Github →
2019-11-18 10:15
src/data/finset.lean
feat(data/finset): new union, set difference, singleton lemmas (#1702) …
Added finset.union_sdiff_self_eq_unionView on Github →