setOf_liouville — Mathlib

English

The set of Liouville numbers is IsGδ (a countable intersection of open sets).

Русский

Множество чисел Лиувилля является IsGδ (счётное пересечение открытых множеств).

LaTeX

$$$$ IsG\delta\big(\{ x : Liouville(x) \} \big). $$$$

Lean4

theorem setOf_liouville : IsGδ {x | Liouville x} :=
  by
  rw [setOf_liouville_eq_iInter_iUnion]
  refine .iInter fun n => IsOpen.isGδ ?_
  refine isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_
  exact isOpen_ball.inter isClosed_singleton.isOpen_compl

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