continuousOn_of_continuousOn_uncurry

English

The neighborhood filter at f in the compact-open topology equals the infimum of the induced neighborhood filters from the restrictions to compact subsets.

Русский

Фильтр окрестностей nhds(f) в компактно-открытой топологии равен инфимуму индуцированных фильтров окрестностей от ограничений к компактным подмножествам.

LaTeX

$$$\nhds f = \bigwedge_{K} \; (\nhds (f\restriction K)).\text{comap}(\restrict K)$$$

Lean4

theorem continuousOn_of_continuousOn_uncurry {s : Set X} (f : X → C(Y, Z))
    (h : ContinuousOn (Function.uncurry fun x y => f x y) (s ×ˢ univ)) : ContinuousOn f s :=
  continuousOn_iff_continuous_restrict.mpr <|
    continuous_of_continuous_uncurry _ <|
      h.comp_continuous (continuous_subtype_val.prodMap continuous_id) (fun x ↦ ⟨x.1.2, trivial⟩)

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