α : Type u_2
β : Type ?u.6936
γ : Type ?u.6939
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (∀ (i : ι), i ∈ insert a s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ insert a s), f i)
α : Type u_2
β : Type ?u.6936
γ : Type ?u.6939
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)
refine' Finite.induction_on hs (by simp) _ h
α : Type u_2
β : Type ?u.6936
γ : Type ?u.6939
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (IsGδ (f a) ∧ ∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (f a ∪ ⋃ (i : ι) (_ : i ∈ s), f i)
α : Type u_2
β : Type ?u.6936
γ : Type ?u.6939
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (∀ (i : ι), i ∈ insert a s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ insert a s), f i)
simp only [ball_insert_iff, biUnion_insert]
no goals
α : Type u_2
β : Type ?u.6936
γ : Type ?u.6939
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (IsGδ (f a) ∧ ∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (f a ∪ ⋃ (i : ι) (_ : i ∈ s), f i)
exact fun _ _ ihs H => H.1.union (ihs H.2)
no goals
α : Type u_2
β : Type ?u.6936
γ : Type ?u.6939
ι : Type u_1
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ (∀ (i : ι), i ∈ ∅ → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ ∅), f i)
simp