prodMk_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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