Theorem Filter.set_eventuallyEq_iff_inf_principal

Modification history

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 →