comp — Mathlib

English

If g: γ → δ is uniformly continuous and f: α → β → γ is uniformly continuous in two arguments, then the two-argument composition g ∘₂ f: α × β → δ is uniformly continuous.

Русский

Если g: γ → δ равномерно непрерывна, а f: α → β → γ равномерно непрерывна во всех двух аргументах, то двухаргументационная композиция g ∘₂ f: α × β → δ равномерно непрерывна.

LaTeX

$$$\\operatorname{UniformContinuous}(g) \\to \\operatorname{UniformContinuous}_2(f) \\to \\operatorname{UniformContinuous}_2(g \\circ_2 f)$$$

Lean4

theorem comp {f : α → β → γ} {g : γ → δ} (hg : UniformContinuous g) (hf : UniformContinuous₂ f) :
    UniformContinuous₂ (g ∘₂ f) :=
  hg.comp hf

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