⊢ IsGδ (⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
⊢ IsGδ {x | Liouville x}
rw [setOf_liouville_eq_iInter_iUnion]
n : ℕ
⊢ IsOpen (⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
⊢ IsGδ (⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
refine isGδ_iInter fun n => IsOpen.isGδ ?_
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen (ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
n : ℕ
⊢ IsOpen (⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
refine isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_
no goals
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen (ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
exact isOpen_ball.inter isClosed_singleton.isOpen_compl