range_list_getI — Mathlib

English

Let l be a list with an Inhabited α (i.e., there is a default element). Then the range of l.getI is the union of the default element with all elements of l: range l.getI = insert default { x | x ∈ l }.

Русский

Пусть l — список α и существует элемент по умолчанию в α. Тогда множество значений l.getI равно {default} ∪ { x : x ∈ l }.

LaTeX

$$$\\operatorname{range} l.getI = \\operatorname{insert} \\operatorname{default} \\{ x \\mid x \\in l \\}.$$$

Lean4

@[simp]
theorem range_list_getI [Inhabited α] (l : List α) : range l.getI = insert default {x | x ∈ l} :=
  by
  unfold List.getI
  simp

Похожие утверждения