Commit 2022-12-14 02:53 4aa4f3dc

View on Github →

feat port: data.set.bool_indicator (#988) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/BoolIndicator.lean

added theorem Set.mem_iff_boolIndicator

added theorem Set.not_mem_iff_boolIndicator

added theorem Set.preimage_boolIndicator

added theorem Set.preimage_boolIndicator_eq_union

added theorem Set.preimage_boolIndicator_false

added theorem Set.preimage_boolIndicator_true