list.nth_le_map_rev

A version of nth_le_map that can be used for rewriting.

list.pmap

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy p, using the proof to apply f.

list.attach

"Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

list.Ico

Ico n m is the list of natural numbers n ≤ x < m. (Ico stands for "interval, closed-open".)

See also data/set/intervals.lean for set.Ico, modelling intervals in general preorders, and multiset.Ico and finset.Ico for n ≤ x < m as a multiset or as a finset.

@TODO (anyone): Define Ioo and Icc, state basic lemmas about them. @TODO (anyone): Prove that finset.Ico and set.Ico agree. @TODO (anyone): Also do the versions for integers? @TODO (anyone): One could generalise even further, defining 'locally finite partial orders', for which set.Ico a b is [finite], and 'locally finite total orders', for which there is a list model.

list.nat.antidiagonal

The antidiagonal of a natural number n is the list of pairs (i,j) such that i+j = n.

list.nat.mem_antidiagonal

A pair (i,j) is contained in the antidiagonal of n if and only if i+j=n.

list.nat.length_antidiagonal

The length of the antidiagonal of n is n+1.

list.nat.antidiagonal_zero

The antidiagonal of 0 is the list [(0,0)]

list.nat.nodup_antidiagonal

The antidiagonal of n does not contain duplicate entries.