uniformContinuous — Mathlib

English

A function f: β → Matrix m n 𝕜 is uniformly continuous iff each coordinate map i,j: x ↦ f(x)_{i j} is uniformly continuous.

Русский

Функция f: β → Matrix m n 𝕜 равномерно непрерывна тогда и только когда все координатные отображения i,j: x ↦ f(x)_{i j} равномерно непрерывны.

LaTeX

$$$\UniformContinuous f \ \Leftrightarrow\ \forall i,j,\ UniformContinuous (\lambda x. f\,x)_{i j}$$$

Lean4

theorem uniformContinuous {β : Type*} [UniformSpace β] {f : β → Matrix m n 𝕜} :
    UniformContinuous f ↔ ∀ i j, UniformContinuous fun x => f x i j :=
  by
  simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]
  apply Iff.intro <;> intro a <;> apply a

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