Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.filter_gt_eq_Iio

Modification history

2022-06-15 13:13

src/data/finset/locally_finite.lean

refactor(order/locally_finite): Allow `finset.Iix`/`finset.Ixi` on empty types (#14430) …

Modified finset.filter_gt_eq_Iio View on Github →

2022-01-28 13:31

src/data/finset/locally_finite.lean

chore(order/locally_finite): fill in finset interval API (#11338) …

Modified finset.filter_gt_eq_Iio View on Github →

2021-12-30 14:54

src/data/finset/locally_finite.lean

feat(data/fin/interval): add lemmas (#11102) …

Added finset.filter_gt_eq_Iio View on Github →