curry_right — Mathlib

English

Let f: X × Y → Z be continuous. Then for every x ∈ X, the map y ↦ f(x, y) is continuous.

Русский

Пусть f: X × Y → Z непрерывна. Тогда для каждого x ∈ X отображение y ↦ f(x, y) непрерывно.

LaTeX

$$$$\mathrm{Continuous}(f) \Rightarrow \forall x \in X,\ \mathrm{Continuous}(y \mapsto f(x,y)).$$$$

Lean4

/-- Continuous functions on products are continuous in their second argument -/
theorem curry_right {f : X × Y → Z} (hf : Continuous f) {x : X} : Continuous fun y ↦ f (x, y) :=
  hf.comp (.prodMk_right _)

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