uniformEquicontinuousOn — Mathlib

English

If a family f: α → γ → β is pointwise Lipschitz on s with a common constant K, then the family is uniformly equicontinuous on s.

Русский

Если семейство функций f: α → γ → β имеет единый констант липшицевости K на s по каждому аргументу, то это семейство эквиконтинуально равномерно непрерывно на s.

LaTeX

$$(∀ c, LipschitzOnWith K (f c) s) → UniformEquicontinuousOn f s$$

Lean4

/-- If `f : α → γ → β` is a family of a functions, all of which are Lipschitz on `s` with the
same constant, then the family is uniformly equicontinuous on `s`. -/
theorem _root_.LipschitzOnWith.uniformEquicontinuousOn (f : α → γ → β) (K : ℝ≥0) {s : Set γ}
    (h : ∀ c, LipschitzOnWith K (f c) s) : UniformEquicontinuousOn f s :=
  by
  rw [uniformEquicontinuousOn_iff_uniformContinuousOn]
  rw [← lipschitzOnWith_ofFun_iff] at h
  exact h.uniformContinuousOn

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