Commit 2022-12-26 00:09 88e07e98

View on Github →

feat: port Data.Set.Accumulate (#1210) Relevant Zulip topic

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Accumulate.lean

added def Set.Accumulate

added theorem Set.accumulate_def

added theorem Set.bunionᵢ_accumulate

added theorem Set.mem_accumulate

added theorem Set.monotone_accumulate

added theorem Set.subset_accumulate

added theorem Set.unionᵢ_accumulate