Theorems · Theorem · logic and foundations

Cardinal.cantorFunction_succ

∀ {c : ℝ} (f : ℕ → Bool),
  0 ≤ c →
    c < 1 → Cardinal.cantorFunction c f = (bif f 0 then 1 else 0) + c * Cardinal.cantorFunction c fun n => f (n + 1)

Defined in

Mathlib.Analysis.Real.Cardinality

Cited by

1 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound