subset_range_enumerate — Mathlib

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]⟩

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