Theorem Filter.set_eventuallyEq_iff_inf_principal

Modification history

2026-08-27 10:24
Mathlib/Order/Filter/Basic.lean
refactor: definition and notation for `EventuallyEq` on `Set` (#41533) …
Deleted Filter.set_eventuallyEq_iff_inf_principalView on Github →
2023-05-25 11:48
Mathlib/Order/Filter/Basic.lean
feat: forward-port PR 19070 (#4327) …
Added Filter.set_eventuallyEq_iff_inf_principalView on Github →