Theorems · Theorem · logic and foundations

Cardinal.increasing_cantorFunction

∀ {c : ℝ},
  0 < c →
    c < 1 / 2 →
      ∀ {n : ℕ} {f g : ℕ → Bool},
        (∀ k < n, f k = g k) → f n = false → g n = true → Cardinal.cantorFunction c f < Cardinal.cantorFunction c g

cantorFunction c is strictly increasing with if 0 < c < 1/2, if we endow ℕ → Bool with a lexicographic order. The lexicographic order doesn't exist for these infinitary products, so we explicitly write out what it means.

Defined in

Mathlib.Analysis.Real.Cardinality

Cited by

1 results in Mathlib

Foundations

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