Commit 2023-12-20 15:54 fb0bfc6b

View on Github →

feat(Order/Filter): add lemmas about Eventually* and iInter/iUnion (#9090) As requested by Terence Tao on Zulip

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

added theorem Finset.eventuallyEq_iInter

added theorem Finset.eventuallyEq_iUnion

added theorem Finset.eventuallyLE_iInter

added theorem Finset.eventuallyLE_iUnion

added theorem Set.Finite.eventuallyEq_iInter

added theorem Set.Finite.eventuallyEq_iUnion

added theorem Set.Finite.eventuallyLE_iInter

added theorem Set.Finite.eventuallyLE_iUnion