Theorem Finset.insert_erase_eq_insert

Modification history

2026-08-12 08:59
Mathlib/Data/Finset/Basic.lean
feat(Data/Finset): `insert a (s.erase a) = insert a s` (#40775)
Added Finset.insert_erase_eq_insertView on Github →