prodMk_left — Mathlib

English

If f is uniformly continuous, then a ↦ f(a,b) is uniformly continuous for fixed b.

Русский

Если f равномерно непрерывна, то для фиксированного b отображение a ↦ f(a,b) равномерно непрерывно.

LaTeX

$$$\text{UniformContinuous}(f) \Rightarrow \forall b, \text{UniformContinuous}(a \mapsto f(a,b))$$$

Lean4

theorem prodMk_left {f : α × β → γ} (h : UniformContinuous f) (b) : UniformContinuous fun a => f (a, b) :=
  h.comp (uniformContinuous_id.prodMk uniformContinuous_const)

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