ι : Type u_1
ι' : Type ?u.8425
α : Type ?u.8428
X : Type u_2
Y : Type ?u.8434
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), f iᶜ)
ι : Type u_1
ι' : Type ?u.8425
α : Type ?u.8428
X : Type u_2
Y : Type ?u.8434
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ (⋂ (i : ι) (_ : ¬x ∈ f i), f iᶜ) ∈ 𝓝 x
refine' IsOpen.mem_nhds _ (mem_iInter₂.2 fun i => id)
ι : Type u_1
ι' : Type ?u.8425
α : Type ?u.8428
X : Type u_2
Y : Type ?u.8434
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
ι : Type u_1
ι' : Type ?u.8425
α : Type ?u.8428
X : Type u_2
Y : Type ?u.8434
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), f iᶜ)
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by
  rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
no goals
ι : Type u_1
ι' : Type ?u.8425
α : Type ?u.8428
X : Type u_2
Y : Type ?u.8434
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _
no goals
ι : Type u_1
ι' : Type ?u.8425
α : Type ?u.8428
X : Type u_2
Y : Type ?u.8434
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
this : IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), f iᶜ)
rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this