cantorFunctionAux — Mathlib

English

The Cantor function auxiliary is defined by placing c^n at position n when the nth bit is true, and 0 when it is false.

Русский

Вспомогательная функция Кантора задается так: в позиции n ставим c^n если n-й бит равен истине, иначе 0.

LaTeX

$$CantorFunctionAux$(c,f,n)=\\begin{cases} c^n, & f(n)=\\text{true} \\\\ 0, & f(n)=\\text{false} \\end{cases}$$$

Lean4

/-- The body of the sum in `cantorFunction`.
`cantorFunctionAux c f n = c ^ n` if `f n = true`;
`cantorFunctionAux c f n = 0` if `f n = false`. -/
def cantorFunctionAux (c : ℝ) (f : ℕ → Bool) (n : ℕ) : ℝ :=
  cond (f n) (c ^ n) 0

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