uniformContinuous_pi — Mathlib

English

A function f: β → ∀ i, α i is uniformly continuous iff each projection coordinate i yields a uniformly continuous map x ↦ f x i.

Русский

Функция f: β → ∀ i, α i равномерно непрерывна тогда и только тогда, когда каждая координатная проекция i образует равномерно непрерывный отображение x ↦ f x i.

LaTeX

$$$\ UniformContinuous f \iff \forall i, UniformContinuous (\lambda x, f x i)$$$

Lean4

theorem uniformContinuous_pi {β : Type*} [UniformSpace β] {f : β → ∀ i, α i} :
    UniformContinuous f ↔ ∀ i, UniformContinuous fun x => f x i := by
  simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp_def]

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