no goals
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
classical
  refine' s.induction_on (by simp) _
  intro i s _ h₂
  simp [h₂]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      (closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)) →
        closure (⋃ (i : ι) (_ : i ∈ insert a s), f i) = ⋃ (i : ι) (_ : i ∈ insert a s), closure (f i)
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
refine' s.induction_on (by simp) _
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s✝ : Finset ι
f : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h₂ : closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
⊢ closure (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), f i_1) = ⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), closure (f i_1)
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      (closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)) →
        closure (⋃ (i : ι) (_ : i ∈ insert a s), f i) = ⋃ (i : ι) (_ : i ∈ insert a s), closure (f i)
intro i s _ h₂
no goals
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s✝ : Finset ι
f : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h₂ : closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
⊢ closure (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), f i_1) = ⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), closure (f i_1)
simp [h₂]
no goals
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ closure (⋃ (i : ι) (_ : i ∈ ∅), f i) = ⋃ (i : ι) (_ : i ∈ ∅), closure (f i)
simp