Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.subset_insert_iff_of_not_mem

Modification history

2023-02-24 15:00
src/data/set/basic.lean
chore(data/set/basic): Golf #18356 (#18491) …
Modified set.subset_insert_iff_of_not_memView on Github →
2023-02-22 15:42
src/data/set/basic.lean
feat(data/set): add lemmas about `powerset` of `insert` and `singleton` (#18356) …
Added set.subset_insert_iff_of_not_memView on Github →