α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), IsOpen (s iᶜ)
⊢ IsOpen (⋂ (i : ι), s iᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), IsClosed (s i)
⊢ IsClosed (⋃ (i : ι), s i)
simp only [← isOpen_compl_iff, compl_iUnion] at *
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), IsOpen (s iᶜ)
⊢ IsOpen (⋂ (i : ι), s iᶜ)
exact isOpen_iInter h