curry_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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