continuous_of_continuous_uncurry — Mathlib

English

The compact-open topology equals the infimum of induced topologies for all compact subsets; a variant of the previous statement.

Русский

Компактно-открытая топология равна инфимуму индуцированных топологий по всем компактным подмножества X (вариант утверждения).

LaTeX

$$$\text{compactOpen} = \bigwedge_{K:\, Set X,\ IsCompact K} \.induced(\text{restrict}_K) \text{compactOpen}$$$

Lean4

/-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form
α × β → γ` is continuous. -/
theorem continuous_of_continuous_uncurry (f : X → C(Y, Z)) (h : Continuous (Function.uncurry fun x y => f x y)) :
    Continuous f :=
  (curry ⟨_, h⟩).2

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