Theorem LE.le.eventuallyLE

Modification history

2026-08-27 10:24

Mathlib/Order/Filter/Basic.lean

refactor: definition and notation for `EventuallyEq` on `Set` (#41533) …

Modified LE.le.eventuallyLE View on Github →

2026-07-06 15:50

Mathlib/Order/Filter/Basic.lean

feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet`, `Class` (#32983) …

Added LE.le.eventuallyLE View on Github →