English
For every n, 1/4 and 3/4 belong to preCantorSet n.
Русский
Для каждого n точки 1/4 и 3/4 принадлежат preCantorSet n.
LaTeX
$$$\forall n,\ 1/4 \in \text{preCantorSet}(n) \wedge 3/4 \in \text{preCantorSet}(n).$$$
Lean4
theorem quarters_mem_preCantorSet (n : ℕ) : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n := by
induction n with
| zero =>
simp only [preCantorSet_zero]
refine ⟨⟨?_, ?_⟩, ?_, ?_⟩ <;> norm_num
| succ n ih =>
apply And.intro
· -- goal: 1 / 4 ∈ preCantorSet (n + 1)
-- follows by the inductive hypothesis, since 3 / 4 ∈ preCantorSet n
exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩
· -- goal: 3 / 4 ∈ preCantorSet (n + 1)
-- follows by the inductive hypothesis, since 1 / 4 ∈ preCantorSet n
exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩
