Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.insert_diff_eq_singleton

Modification history

2022-03-12 18:01
src/data/set/basic.lean
feat(order/complete_lattice): add `complete_lattice.independent_pair` (#12565) …
Added set.insert_diff_eq_singletonView on Github →