instRegularSpace — Mathlib

English

If Y is a Regular space, then C(X,Y) is Regular.

Русский

Если Y регулярное пространство, то C(X,Y) регулярное.

LaTeX

$$$[RegularSpace Y] \\Rightarrow RegularSpace(C(X,Y))$$$

Lean4

instance [RegularSpace Y] : RegularSpace C(X, Y) :=
  .of_lift'_closure_le fun f ↦ by
    rw [← tendsto_id', tendsto_nhds_compactOpen]
    intro K hK U hU hf
    rcases (hK.image f.continuous).exists_isOpen_closure_subset (hU.mem_nhdsSet.2 hf.image_subset) with
      ⟨V, hVo, hKV, hVU⟩
    filter_upwards [mem_lift' (eventually_mapsTo hK hVo (mapsTo_iff_image_subset.2 hKV))] with g hg
    refine ((isClosed_setOf_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU
    exact closure_mono (fun _ h ↦ h.mono_right subset_closure) hg

Похожие утверждения