English
If each X_i is R1 space, then the space of all functions i → X_i is R1.
Русский
Если каждый X_i является R1-пространством, то пространство всех функций i → X_i тоже R1-пространство.
LaTeX
$$R1Space((i → X_i))$$
Lean4
theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
[R1Space Y] {f : X → Y} {x : X} {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ 𝓝 (f x)) (hKc : IsCompact K)
(hKx : K ∈ 𝓝 x) : ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s :=
by
have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior
obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) :=
by
simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
disjoint_nhds_nhds_iff_not_inseparable]
rintro y ⟨-, hys⟩ hxy
refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
rwa [mem_interior_iff_mem_nhds]
refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩
· filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx using Set.disjoint_left.1 hd hx
· by_contra hys
exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, notMem_subset interior_subset hys⟩)
