Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.eventually_le.union

Modification history

2021-01-10 14:47

src/order/filter/basic.lean

chore(order/filter): a few more lemmas about `eventually` and set operations (#5686)

Added filter.eventually_le.union View on Github →