English
If s is countable with default, every element of s belongs to the range of enumerateCountable.
Русский
Если s счётно и задан дефолт, каждое элемент s принадлежит диапазону enumerateCountable.
LaTeX
$$$s.Countable \Rightarrow s \subseteq \mathrm{range}(\operatorname{enumerateCountable}(s,h,default))$$$
Lean4
theorem subset_range_enumerate {s : Set α} (h : s.Countable) (default : α) : s ⊆ range (enumerateCountable h default) :=
fun x hx => ⟨@Encodable.encode s h.toEncodable ⟨x, hx⟩, by simp [enumerateCountable, Encodable.encodek]⟩