instLipschitzAdd — Mathlib

English

There is a LipschitzAdd structure on the space of bounded continuous functions: the map (f,g) ↦ f+g is Lipschitz with a universal constant depending on the bound in the codomain.

Русский

На пространстве ограниченных непрерывных функций существует структура LipschitzAdd: сумма функций является Lipschitz-преобразованием.

LaTeX

$$$\text{LipschitzAdd}(\alpha \to^{\mathrm{b}} \beta)$$$

Lean4

instance instLipschitzAdd : LipschitzAdd (α →ᵇ β) where
  lipschitz_add :=
    ⟨LipschitzAdd.C β, by
      have C_nonneg := (LipschitzAdd.C β).coe_nonneg
      rw [lipschitzWith_iff_dist_le_mul]
      rintro ⟨f₁, g₁⟩ ⟨f₂, g₂⟩
      rw [dist_le (mul_nonneg C_nonneg dist_nonneg)]
      intro x
      refine le_trans (lipschitz_with_lipschitz_const_add ⟨f₁ x, g₁ x⟩ ⟨f₂ x, g₂ x⟩) ?_
      gcongr
      apply max_le_max <;> exact dist_coe_le_dist x⟩

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