English
The range of the function l[·]? : ℕ → Option α is the set consisting of none and some elements corresponding to l, i.e., none together with some {x | x ∈ l}.
Русский
Область значений функции l[·]? : ℕ → Option α состоит из none и некоторых элементов, соответствующих l, то есть none вместе с some {x | x ∈ l}.
LaTeX
$$$\\text{range}(l[\\cdot]? : \\mathbb{N} \\to \\text{Option } \\alpha) = \\text{insert none } (\\text{Some } '' \\{x \\mid x \\in l\\})$$$
Lean4
theorem range_list_getElem? : range (l[·]? : ℕ → Option α) = insert none (some '' {x | x ∈ l}) :=
by
rw [← range_list_get, ← range_comp]
refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
· exact (le_or_gt l.length n).imp getElem?_eq_none_iff.mpr (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)
· exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩
· exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩
