case intro.intro.mk
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ s
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
⊢ IsGδ s
rcases(@uniformity_hasBasis_open α _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
case intro.intro.mk
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ) (_ : True), ⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U i)))
case intro.intro.mk
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ s
rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
case intro.intro.mk
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
n : ℕ
x✝ : n ∈ fun i => True
⊢ IsOpen (⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U n)))
case intro.intro.mk
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ) (_ : True), ⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U i)))
refine' isGδ_biInter (to_countable _) fun n _ => IsOpen.isGδ _
no goals
case intro.intro.mk
α✝ : Type ?u.10695
β : Type ?u.10698
γ : Type ?u.10701
ι : Type ?u.10704
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
n : ℕ
x✝ : n ∈ fun i => True
⊢ IsOpen (⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U n)))
exact isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2