Commit 2026-09-03 20:16 30a58f79

refactor: definition for EventuallyConst on Set (#43114) Introduce definition EventuallyEmptyOrUniv as the Set version of EventuallyConst. In mathlib, we currently use EventuallyConst for sets, which abuses the Set α := α → Prop defeq and which will break once we make Set a one-field structure. Generated by Claude Sonnet, reviewed line by line by myself. Assisted-by: Claude Sonnet 5