α : Type u_2
β : Type ?u.5171
γ : Type ?u.5174
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
α : Type u_2
β : Type ?u.5171
γ : Type ?u.5174
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (i : ι) (h : i ∈ s), t i h)
rw [biInter_eq_iInter]
α : Type u_2
β : Type ?u.5171
γ : Type ?u.5174
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Encodable ↑s
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
α : Type u_2
β : Type ?u.5171
γ : Type ?u.5174
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
haveI := hs.toEncodable
no goals
α : Type u_2
β : Type ?u.5171
γ : Type ?u.5174
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Encodable ↑s
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
exact isGδ_iInter fun x => ht x x.2