diff --git a/Mathlib/Analysis/Real/OfDigits.lean b/Mathlib/Analysis/Real/OfDigits.lean
index f206d72c68..03d3f34dc5 100644
--- a/Mathlib/Analysis/Real/OfDigits.lean
+++ b/Mathlib/Analysis/Real/OfDigits.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasilii Nesterov
 -/
 import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Analysis.Normed.Group.FunctionSeries
 import Mathlib.Analysis.SpecificLimits.Normed
 import Mathlib.Tactic.Rify
 
@@ -101,6 +102,35 @@ theorem abs_ofDigits_sub_ofDigits_le {b : ℕ} {x y : ℕ → Fin b} {n : ℕ}
     (ofDigits_nonneg _) (ofDigits_le_one _)
   simp
 
+/-- Interpreting a sequence of digits as a real number is continuous. -/
+theorem continuous_ofDigits (b : ℕ) : Continuous (ofDigits : (ℕ → Fin b) → ℝ) := by
+  rcases b with _ | b
+  · letI : IsEmpty (ℕ → Fin 0) := ⟨fun x ↦ Fin.elim0 (x 0)⟩
+    rw [continuous_def]
+    intro s hs
+    convert isOpen_empty
+    exact Set.eq_empty_iff_forall_notMem.mpr fun x _ ↦ isEmptyElim x
+  · rcases b with _ | b
+    · convert (continuous_const : Continuous fun _ : ℕ → Fin 1 ↦ (0 : ℝ)) using 1
+      funext x
+      simp [ofDigits, ofDigitsTerm]
+    change Continuous fun x : ℕ → Fin (b + 2) ↦ ∑' n, ofDigitsTerm x n
+    apply continuous_tsum (u := fun n ↦ (b + 1 : ℝ) * ((b + 2 : ℝ) ^ (n + 1))⁻¹)
+    · intro n
+      unfold ofDigitsTerm
+      fun_prop
+    · simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
+      exact Summable.mul_left _ <| summable_geometric_of_lt_one (by positivity) (by
+        apply (inv_lt_one₀ (by positivity)).mpr
+        have : 0 ≤ (b : ℝ) := by positivity
+        linarith)
+    · intro n x
+      rw [Real.norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg]
+      have h := ofDigitsTerm_le (digits := x) (n := n)
+      norm_num [Nat.cast_add, Nat.cast_ofNat] at h ⊢
+      convert h using 1
+      ring
+
 /-- Converts a real number `x` from the interval `[0, 1)` into sequence of
 its digits in base `b`. -/
 noncomputable def digits (x : ℝ) (b : ℕ) [NeZero b] : ℕ → Fin b :=
diff --git a/Mathlib/Topology/Instances/CantorSet.lean b/Mathlib/Topology/Instances/CantorSet.lean
index a1a1324c55..d5f35045aa 100644
--- a/Mathlib/Topology/Instances/CantorSet.lean
+++ b/Mathlib/Topology/Instances/CantorSet.lean
@@ -29,6 +29,8 @@ This file defines the Cantor ternary set and proves a few properties.
 * `ofDigits_zero_two_sequence_mem_cantorSet`: any such sequence corresponds to a number
   in the Cantor set.
 * `ofDigits_zero_two_sequence_unique`: such a representation is unique.
+* `cantorSetHomeomorph`: the ternary Cantor set is homeomorphic to the space of infinite
+  Boolean sequences.
 -/
 
 /-- The order `n` pre-Cantor set, defined starting from `[0, 1]` and successively removing the
@@ -312,4 +314,41 @@ theorem cantorSet_eq_zero_two_ofDigits :
   · rw [← ha.right]
     exact ofDigits_zero_two_sequence_mem_cantorSet ha.left
 
+/-- The ternary Cantor set is homeomorphic to the space of infinite Boolean sequences. -/
+noncomputable def cantorSetHomeomorph : cantorSet ≃ₜ (ℕ → Bool) := by
+  let ternary : (ℕ → Bool) → ℕ → Fin 3 := fun a n ↦ if a n then 2 else 0
+  have ternary_ne_one (a : ℕ → Bool) (n : ℕ) : ternary a n ≠ 1 := by
+    simp only [ternary]
+    split <;> simp_all
+  let toCantor : (ℕ → Bool) → cantorSet := fun a ↦
+    ⟨ofDigits (ternary a), ofDigits_zero_two_sequence_mem_cantorSet (ternary_ne_one a)⟩
+  let toBinary : cantorSet → ℕ → Bool := fun x ↦ (cantorToBinary x).get
+  have toCantor_toBinary (x : cantorSet) : toCantor (toBinary x) = x := by
+    apply Subtype.ext
+    change ofDigits (ternary (toBinary x)) = x
+    rw [show ternary (toBinary x) = (cantorToTernary x).get by
+      funext n
+      simp [ternary, toBinary, cantorToTernary, Stream'.get_map]]
+    exact ofDigits_cantorToTernary x.property
+  have toBinary_toCantor (a : ℕ → Bool) : toBinary (toCantor a) = a := by
+    have hternary : (cantorToTernary (toCantor a)).get = ternary a :=
+      ofDigits_zero_two_sequence_unique (fun _ ↦ cantorToTernary_ne_one)
+        (ternary_ne_one a) (by
+          rw [ofDigits_cantorToTernary (toCantor a).property])
+    funext n
+    have hn := congrFun hternary n
+    simp only [cantorToTernary, Stream'.get_map, ternary] at hn
+    grind
+  let e : (ℕ → Bool) ≃ cantorSet :=
+    { toFun := toCantor
+      invFun := toBinary
+      left_inv := toBinary_toCantor
+      right_inv := toCantor_toBinary }
+  have he : Continuous e := by
+    apply Continuous.subtype_mk
+    exact (Real.continuous_ofDigits 3).comp <| continuous_pi fun n ↦ by
+      exact (continuous_of_discreteTopology : Continuous fun b : Bool ↦
+        if b then (2 : Fin 3) else 0).comp (continuous_apply n)
+  exact (e.toHomeomorphOfContinuousClosed he he.isClosedMap).symm
+
 end ternary02