setOf_liouville_eq_iInter_iUnion — Mathlib

English

The Liouville set equals the intersection of the irrationals with a certain family of rational-approximation neighborhoods around rationals a/b with b>1, across all n.

Русский

Множество Лиувилля равно пересечению иррациональных чисел с определенной семейством окрестностей приближений рациональных a/b со знаменателем b>1 для всех n.

LaTeX

$$$$ \{ x : \text{Liouville}(x) \} = \{ x : \text{Irrational}(x) \} \cap \bigcap_{n \in \mathbb{N}} \bigcup_{a,b \in \mathbb{Z},\; 1 < b} \mathsf{Ball}\Big(\frac{a}{b}, \frac{1}{b^n}\Big). $$$$

Lean4

theorem setOf_liouville_eq_iInter_iUnion :
    {x | Liouville x} = ⋂ n : ℕ, ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball ((a : ℝ) / b) (1 / (b : ℝ) ^ n) \ {(a : ℝ) / b} :=
  by
  ext x
  simp only [mem_iInter, mem_iUnion, Liouville, mem_setOf_eq, exists_prop, mem_diff, mem_singleton_iff, mem_ball,
    Real.dist_eq, and_comm]

Похожие утверждения