Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.Ico.filter_le_of_le

Modification history

2021-10-08 07:32

src/data/finset/intervals.lean

refactor(data/*/interval): generalize `finset.Ico` to locally finite orders (#7987) …

Deleted finset.Ico.filter_le_of_le View on Github →

2020-07-01 10:05

src/data/finset/basic.lean

chore(data/finset, data/multiset): split into smaller files (#3256) …

Modified finset.Ico.filter_le_of_le View on Github →

2019-09-14 05:00

src/data/finset.lean

chore(data/*): flipping inequalities (#1436) …

Added finset.Ico.filter_le_of_le View on Github →