Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.succ_above_lt_iff

Modification history

2020-11-10 11:25

src/data/fin.lean

feat(data/fin): define `fin.insert_nth` (#4947) …

Modified fin.succ_above_lt_iff View on Github →

2020-09-10 16:46

src/data/fin.lean

feat(data/fin): iffs about succ_above ordering (#4092) …

Added fin.succ_above_lt_iff View on Github →