c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ Summable (cantorFunctionAux c f)
apply (summable_geometric_of_lt_1 h1 h2).summable_of_eq_zero_or_self
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
intro n
no goals
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
cases h : f n <;> simp [h]