Theorem Filter.Eventually.exists_lt

Modification history

2023-10-30 03:09
Mathlib/Topology/Algebra/Order/LeftRight.lean
feat: `โˆƒแถ  x in ๐“ a, x < a` (#7941) โ€ฆ
Modified Filter.Eventually.exists_ltView on Github โ†’
2023-02-05 17:41
Mathlib/Topology/Order/Basic.lean
feat: port Topology.Order.Basic (#2052)
Added Filter.Eventually.exists_ltView on Github โ†’