Commit 2026-08-27 10:24 e7b8da83

refactor: definition and notation for EventuallyEq on Set (#41533) Introduce definitions EventuallyEqSet, EventuallySubset as the Set versions of EventuallyEq and EventuallyLE. Make the notations x =ᶠ[l] y, x ≤ᶠ[l] y x =ᵐ[μ] y. elaborate to either the Set or functiion version depending on the expected type of the argument. In mathlib, we currently use the function predicates for sets, which abuses the Set α := α → Prop defeq and which will break once we make Set a one-field structure. Generated by Claude Opus, reviewed line by line by myself, with a large amount of manual edits and further Claude prompting to polish the angles. Assisted-by: Claude Opus 4.8