Commit 2025-12-14 16:32 772dc6e9

View on Github →

chore: lower case Accumulate (#32871) Accumulate is a function constructing a Set. Per our naming rules, it should be lower-case. The current upper case is probably a consequence of the migration script from Lean 3 to Lean 4, which had issues with the casing of Set-valued functions. This PR changes it to lower case.

Estimated changes

deleted def Set.Accumulate
added def Set.accumulate
modified theorem Set.accumulate_bot
modified theorem Set.accumulate_def
modified theorem Set.accumulate_zero_nat
modified theorem Set.biUnion_accumulate
modified theorem Set.iUnion_accumulate
modified theorem Set.mem_accumulate
modified theorem Set.monotone_accumulate
modified theorem Set.subset_accumulate