case intro
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
cases nonempty_fintype ι
no goals
case intro
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
convert Finset.univ.closure_biUnion f <;> simp