enumerateCountable — Mathlib

English

Noncomputably enumerate elements in a countable set s; the function takes a default element to fill gaps.

Русский

Перечисление элементов множества s с использованием невычислимого перечисления; функция принимает дефолтный элемент для заполнения пропусков.

LaTeX

$$$\operatorname{enumerateCountable} : \{s : \text{Set}(\alpha) \mid s.Countable\} \to (\mathbb{N} \to \alpha)$$$

Lean4

/-- Noncomputably enumerate elements in a set. The `default` value is used to extend the domain to
all of `ℕ`. -/
def enumerateCountable {s : Set α} (h : s.Countable) (default : α) : ℕ → α := fun n =>
  match @Encodable.decode s h.toEncodable n with
  | some y => y
  | none => default

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