English
Given a set-valued selection function sel, enumerate(s) defines a sequence of elements obtained by repeatedly applying sel to the remaining set after removing the previously chosen elements.
Русский
Дано выборочную функцию sel, отображающую множество в элемент; перечисление определяет последовательность элементов, получаемых повторным применением sel к оставшемуся множеству после удаления ранее выбранных элементов.
LaTeX
$$$\text{Enumerate}_{sel}(s,0) = sel(s),\quad \text{Enumerate}_{sel}(s,n+1) = \text{let } a = sel(s)\text{ in Enumerate}_{sel}(s \setminus \{a\}, n)"$$
Lean4
theorem enumerate_eq_none_of_sel {s : Set α} (h : sel s = none) : ∀ {n}, enumerate sel s n = none
| 0 => by simp [h, enumerate]
| n + 1 => by simp [h, enumerate]
