ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite fun i => closure (f i)
intro x
case intro.intro
ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
rcases hf x with ⟨s, hsx, hsf⟩
case intro.intro
ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
i : ι
hi : i ∈ {i | Set.Nonempty ((fun i => closure (f i)) i ∩ interior s)}
⊢ i ∈ {i | Set.Nonempty (f i ∩ s)}
case intro.intro
ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
refine' ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => _⟩
no goals
case intro.intro
ι : Type u_1
ι' : Type ?u.6925
α : Type ?u.6928
X : Type u_2
Y : Type ?u.6934
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
i : ι
hi : i ∈ {i | Set.Nonempty ((fun i => closure (f i)) i ∩ interior s)}
⊢ i ∈ {i | Set.Nonempty (f i ∩ s)}
exact (hi.mono isOpen_interior.closure_inter).of_closure.mono
  (inter_subset_inter_right _ interior_subset)