Commit 2023-02-22 15:42 45501380

View on Github →

feat(data/set): add lemmas about powerset of insert and singleton (#18356) Add lemmas about 𝒫 {x} and 𝒫 (insert x A). Mathlib4 pair : leanprover-community/mathlib4/pull/2000

Estimated changes

Modified src/data/set/basic.lean

added theorem set.powerset_singleton

added theorem set.subset_insert_iff_of_not_mem

Modified src/data/set/image.lean

added theorem set.powerset_insert