English
Let l be a list of elements of α. For every d ∈ α, the set of values obtained from the function n ↦ l[n] with a default value d (used when n is out of bounds) is exactly the set {d} ∪ { x ∈ α : x ∈ l }.
Русский
Пусть l — список элементов α. Для любого d ∈ α множество значений функции n ↦ l[n] (при отсутствии элемента на позиции n берётся значение по умолчанию d) равно множеству {d} ∪ { x ∈ α : x ∈ l }.
LaTeX
$$$\\operatorname{range}\\Big(n: \\mathbb{N} \\mapsto \\begin{cases} l_n, & n < |l| \\\\ d, & n \\ge |l| \\end{cases}\\Big) = \\operatorname{insert} d \\{ x \\mid x \\in l \\}.$$$
Lean4
@[simp]
theorem range_list_getD (d : α) : (range fun n : Nat => l[n]?.getD d) = insert d {x | x ∈ l} :=
calc
(range fun n => l[n]?.getD d) = (fun o : Option α => o.getD d) '' range (l[·]?) :=
by
simp only [← range_comp, Function.comp_def]
rfl
_ = insert d {x | x ∈ l} := by simp only [Option.getD, range_list_getElem?, image_insert_eq, image_image, image_id']
