uniformEquicontinuous — Mathlib

English

If each f c is K-Lipschitz, then the family f: α → γ → β is UniformEquicontinuous.

Русский

Если для каждого c функция f c является гладко-Lipschitz с константой K, то семья f является UniformEquicontinuous.

LaTeX

$$LipschitzWith(K, f) with ∀ c LipschitzWith(K, f c) ⇒ UniformEquicontinuous(f)$$

Lean4

/-- If `f : α → γ → β` is a family of a functions, all of which are Lipschitz with the
same constant, then the family is uniformly equicontinuous. -/
theorem _root_.LipschitzWith.uniformEquicontinuous (f : α → γ → β) (K : ℝ≥0) (h : ∀ c, LipschitzWith K (f c)) :
    UniformEquicontinuous f := by
  rw [uniformEquicontinuous_iff_uniformContinuous]
  rw [← lipschitzWith_ofFun_iff] at h
  exact h.uniformContinuous

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