Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-21 12:39 f52e952e

View on Github →

feat(data/finset): define finset.Ico.subset_iff (#1574)

Estimated changes

Modified src/data/finset.lean

added theorem finset.Ico.subset_iff

Modified src/data/nat/basic.lean

added theorem nat.le_of_pred_lt