Mathlib Map

Theorems · Definition · logic and foundations

Cardinal.cantorFunctionAux

ℝ → (ℕ → Bool) → ℕ → ℝ

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.

Defined in
Mathlib.Analysis.Real.Cardinality
Cited by
9 results in Mathlib
Foundations
Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cardinal.cantorFunctionAux_false · cited by 6Cardinal.cantorFunctionAu…Cardinal.cantorFunctionAux_true · cited by 5Cardinal.cantorFunctionAu…Cardinal.cantorFunction · cited by 4Cardinal.cantorFunctionCardinal.summable_cantor_function · cited by 2Cardinal.summable_cantor_…Cardinal.cantorFunction_le · cited by 1Cardinal.cantorFunction_leCardinal.cantorFunction_succ · cited by 1Cardinal.cantorFunction_s…Cardinal.cantorFunctionAux_nonneg · cited by 1Cardinal.cantorFunctionAu…Cardinal.cantorFunctionAux_succ · cited by 1Cardinal.cantorFunctionAu…Cardinal.cantorFunctionAux_zero · cited by 1Cardinal.cantorFunctionAu…Cardinal.cantorFunctionAux_eq · cited by 0Cardinal.cantorFunctionAu…Real · cited by 25697RealCardinal.cantorFunctionAuxCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement and proof · cited by 25,697

Cited by10

Results whose statement or proof uses this declaration.