Membership of in-range defaulted lookups

A defaulted lookup l.getD i d at an index i < l.length returns an entry of l. Statements that read lists with getD use this to apply a property of all entries; the general case, where the lookup may return the default, is List.getD_mem_or.

Main results

• List.getD_mem: l.getD i d ∈ l for i < l.length.

theorem List.getD_mem {α : Type u_1} (d : α) {l : List α} {i : ℕ} (hi : i < l.length) : l.getD i d ∈ l

An in-range defaulted lookup returns an entry of the list, whatever the default.