Theorem Finset.eventuallyEq_iUnion

Modification history

2024-11-25 09:04

Mathlib/Order/Filter/Basic.lean

chore: split Order.Filter.Basic, creating Order.Filter.Finite (#19354)

Modified Finset.eventuallyEq_iUnion View on Github →

2023-12-20 15:54

Mathlib/Order/Filter/Basic.lean

feat(Order/Filter): add lemmas about `Eventually*` and `iInter`/`iUnion` (#9090) …

Added Finset.eventuallyEq_iUnion View on Github →