α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set β
f : β → Set α
hs : Set.Finite s
h : ∀ (i : β), i ∈ s → IsOpen (f iᶜ)
⊢ IsOpen (⋂ (i : β) (_ : i ∈ s), f iᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set β
f : β → Set α
hs : Set.Finite s
h : ∀ (i : β), i ∈ s → IsClosed (f i)
⊢ IsClosed (⋃ (i : β) (_ : i ∈ s), f 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 α
s : Set β
f : β → Set α
hs : Set.Finite s
h : ∀ (i : β), i ∈ s → IsOpen (f iᶜ)
⊢ IsOpen (⋂ (i : β) (_ : i ∈ s), f iᶜ)
exact isOpen_biInter hs h