diff --git a/Mathlib/Analysis/Real/OfDigits.lean b/Mathlib/Analysis/Real/OfDigits.lean
index f206d72c68..88342f00e0 100644
--- a/Mathlib/Analysis/Real/OfDigits.lean
+++ b/Mathlib/Analysis/Real/OfDigits.lean
@@ -101,6 +101,34 @@ theorem abs_ofDigits_sub_ofDigits_le {b : ℕ} {x y : ℕ → Fin b} {n : ℕ}
     (ofDigits_nonneg _) (ofDigits_le_one _)
   simp
 
+theorem continuous_ofDigits {b : ℕ} :
+    Continuous (ofDigits : (ℕ → Fin b) → ℝ) := by
+  rw [continuous_iff_continuousAt]
+  intro x
+  change Filter.Tendsto ofDigits (nhds x) (nhds (ofDigits x))
+  rw [Metric.tendsto_nhds]
+  intro ε hε
+  obtain rfl | hb := (Nat.one_le_of_lt (b_pos x)).eq_or_lt
+  · filter_upwards [] with y
+    have hy : y = x := Subsingleton.elim y x
+    subst y
+    simp [hε]
+  have hpow : Filter.Tendsto (fun n : ℕ => ((b : ℝ) ^ n)⁻¹) Filter.atTop (nhds 0) := by
+    simpa [inv_pow] using
+      (tendsto_pow_atTop_nhds_zero_of_abs_lt_one (r := (b : ℝ)⁻¹) (by
+        rw [abs_of_nonneg]
+        · have hb' : (1 : ℝ) < b := by exact_mod_cast hb
+          exact (inv_lt_one₀ (by positivity)).2 hb'
+        positivity))
+  obtain ⟨n, hn⟩ := (Metric.tendsto_atTop.1 hpow ε hε)
+  have hnhds : (Set.Iio n).pi (fun i => {x i}) ∈ nhds x :=
+    set_pi_mem_nhds (Set.finite_Iio n) fun i hi => by
+      exact mem_nhds_iff.2 ⟨{x i}, subset_rfl, isOpen_discrete _, rfl⟩
+  filter_upwards [hnhds] with y hy
+  exact lt_of_le_of_lt (abs_ofDigits_sub_ofDigits_le (fun i hi => by
+    rw [Set.mem_pi] at hy
+    exact hy i hi) (n := n)) (by simpa using hn n le_rfl)
+
 /-- 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..4a53e15de8 100644
--- a/Mathlib/Topology/Instances/CantorSet.lean
+++ b/Mathlib/Topology/Instances/CantorSet.lean
@@ -312,4 +312,44 @@ 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 Boolean sequences. -/
+noncomputable def cantorSetHomeomorphNatBool : cantorSet ≃ₜ (ℕ → Bool) := by
+  let ternary (a : ℕ → Bool) : ℕ → Fin 3 := fun n => if a n then 2 else 0
+  let f : (ℕ → Bool) → cantorSet := fun a =>
+    ⟨ofDigits (ternary a), ofDigits_zero_two_sequence_mem_cantorSet (by
+      intro n
+      cases h : a n <;> simp [ternary, h])⟩
+  have hternary : Continuous ternary := by
+    apply continuous_pi
+    intro n
+    simpa [ternary, Function.comp_def] using
+      ((continuous_of_discreteTopology :
+          Continuous (fun z : Bool => if z then (2 : Fin 3) else 0)).comp (continuous_apply n))
+  have hf : Continuous f := by
+    apply Continuous.subtype_mk
+    exact (Real.continuous_ofDigits).comp hternary
+  have hinj : Function.Injective f := by
+    intro a b hab
+    apply funext
+    intro n
+    have h : ternary a = ternary b :=
+      ofDigits_zero_two_sequence_unique
+        (by intro n; cases h : a n <;> simp [ternary, h])
+        (by intro n; cases h : b n <;> simp [ternary, h])
+        (congrArg Subtype.val hab)
+    have := congrFun h n
+    cases ha : a n <;> cases hb : b n <;> simp [ternary, ha, hb] at this ⊢
+  have hsurj : Function.Surjective f := by
+    intro x
+    let a : ℕ → Bool := fun n => decide ((cantorToTernary x.1).get n = 2)
+    have ha : ternary a = (cantorToTernary x.1).get := by
+      funext n
+      have hn := cantorToTernary_ne_one (x := x.1) (n := n)
+      generalize hd : (cantorToTernary x.1).get n = d at hn ⊢
+      fin_cases d <;> simp [a, ternary, hd] at hn ⊢
+    refine ⟨a, ?_⟩
+    apply Subtype.ext
+    simpa [f, a, ha] using ofDigits_cantorToTernary x.2
+  exact ((hf.isClosedEmbedding hinj).toHomeomorphOfSurjective hsurj).symm
+
 end ternary02