English
The Liouville set equals the intersection of the irrationals with a nested intersection/union of balls around rationals a/b with denominators b.
Русский
Множество Лиувилля равно пересечению иррациональных чисел с вложенным пересечением/объединением мячей вокруг рациональных a/b с знаменателями b.
LaTeX
$$$$ {x : Liouville(x)} = {x : Irrational(x)} \cap \bigcap_{n \in \mathbb{N}} \bigcup_{a,b \in \mathbb{Z},\; 1 < b} Ball\Big(\frac{a}{b}, \frac{1}{b^{n}}\Big). $$$$
Lean4
theorem setOf_liouville_eq_irrational_inter_iInter_iUnion :
{x | Liouville x} = {x | Irrational x} ∩ ⋂ n : ℕ, ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (a / b) (1 / (b : ℝ) ^ n) :=
by
refine Subset.antisymm ?_ ?_
· refine subset_inter (fun x hx => hx.irrational) ?_
rw [setOf_liouville_eq_iInter_iUnion]
exact iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun _hb => diff_subset
· simp only [inter_iInter, inter_iUnion, setOf_liouville_eq_iInter_iUnion]
refine iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun hb => ?_
rw [inter_comm]
exact diff_subset_diff Subset.rfl (singleton_subset_iff.2 ⟨a / b, by norm_cast⟩)
