Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.Ico_subset_Ici_self

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.Ico_subset_Ici_self View on Github →

2022-01-28 13:31

src/data/finset/locally_finite.lean

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

Added finset.Ico_subset_Ici_self View on Github →