English
The Cantor set satisfies C = (C/3) ∪ ((2+x)/3)''C.
Русский
Канторово множество удовлетворяет равенству C = (C/3) ∪ ((2+x)/3)''C.
LaTeX
$$$\text{cantorSet} = (\cdot/3)''\text{cantorSet} \cup (\lambda x. (2+x)/3)''\text{cantorSet}. $$$
Lean4
/-- The ternary Cantor set satisfies the equation `C = C / 3 ∪ (2 / 3 + C / 3)`. -/
theorem cantorSet_eq_union_halves : cantorSet = (· / 3) '' cantorSet ∪ (fun x ↦ (2 + x) / 3) '' cantorSet :=
by
simp only [cantorSet]
rw [Set.image_iInter, Set.image_iInter]
rotate_left
· exact (mulRight_bijective₀ 3⁻¹ (by simp)).comp (AddGroup.addLeft_bijective 2)
· exact mulRight_bijective₀ 3⁻¹ (by simp)
simp_rw [← Function.comp_def, ←
Set.iInter_union_of_antitone (Set.monotone_image.comp_antitone preCantorSet_antitone)
(Set.monotone_image.comp_antitone preCantorSet_antitone),
Function.comp_def, ← preCantorSet_succ]
exact (preCantorSet_antitone.iInter_nat_add _).symm
