cantorFunction — Mathlib

English

CantorFunction c f is defined as the sum over n of CantorFunctionAux c f n.

Русский

CantorFunction c f определяется как сумма по n CantorFunctionAux c f n.

LaTeX

$$$\\operatorname{cantorFunction}(c,f) = \\sum_{n=0}^{\\infty} \\operatorname{cantorFunctionAux}(c,f,n)$$$

Lean4

/-- `cantorFunction c (f : ℕ → Bool)` is `Σ n, f n * c ^ n`, where `true` is interpreted as `1` and
`false` is interpreted as `0`. It is implemented using `cantorFunctionAux`. -/
def cantorFunction (c : ℝ) (f : ℕ → Bool) : ℝ :=
  ∑' n, cantorFunctionAux c f n

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