case intro.intro
α : Type u_1
β : Type ?u.12419
γ : Type ?u.12422
ι : Type ?u.12425
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ {a}
α : Type u_1
β : Type ?u.12419
γ : Type ?u.12422
ι : Type ?u.12425
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
⊢ IsGδ {a}
rcases (nhds_basis_opens a).exists_antitone_subbasis with ⟨U, hU, h_basis⟩
case intro.intro
α : Type u_1
β : Type ?u.12419
γ : Type ?u.12422
ι : Type ?u.12425
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ (⋂ (i : ℕ) (_ : True), U i)
case intro.intro
α : Type u_1
β : Type ?u.12419
γ : Type ?u.12422
ι : Type ?u.12425
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ {a}
rw [← biInter_basis_nhds h_basis.toHasBasis]
no goals
case intro.intro
α : Type u_1
β : Type ?u.12419
γ : Type ?u.12422
ι : Type ?u.12425
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ (⋂ (i : ℕ) (_ : True), U i)
exact isGδ_biInter (to_countable _) fun n _ => (hU n).2.isGδ