α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), s i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), s i)
α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
hs : ∀ (i : ι), IsGδ (s i)
⊢ IsGδ (⋂ (i : ι), s i)
choose T hTo hTc hTs using hs
α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), (fun i => ⋂₀ T i) i)
α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), s i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), s i)
obtain rfl : s = fun i => ⋂₀ T i := funext hTs
α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ (t : Set α), (t ∈ ⋃ (i : ι), T i) → IsOpen t
α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), (fun i => ⋂₀ T i) i)
refine' ⟨⋃ i, T i, _, countable_iUnion hTc, (sInter_iUnion _).symm⟩
no goals
α : Type u_2
β : Type ?u.1911
γ : Type ?u.1914
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ (t : Set α), (t ∈ ⋃ (i : ι), T i) → IsOpen t
simpa [@forall_swap ι] using hTo