lipschitzWith_restrict — Mathlib

English

For a fixed s ∈ 𝔖, the restriction map from (α →ᵤ[𝔖] β) to (s →ᵤ β) given by f ↦ UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖 is 1-Lipschitz.

Русский

Для фиксированного s ∈ 𝔖 отображение ограничения из (α →ᵤ[𝔖] β) в (s →ᵤ β), заданное f ↦ UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖, является 1-липшицевым.

LaTeX

$$$\mathrm{Lipschitz}_1\big(\mathrm{UniformFun.ofFun} \circ s.restrict \circ \mathrm{toFun}_{\mathfrak{S}}\big) : (\alpha \to_{\mathfrak{S}} \beta) \to (s \to_{\beta} \beta)$$$

Lean4

theorem lipschitzWith_restrict (s : Set α) (hs : s ∈ 𝔖) :
    LipschitzWith 1 (UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖 : (α →ᵤ[𝔖] β) → (s →ᵤ β)) :=
  UniformFun.lipschitzWith_iff.mpr fun x ↦ lipschitzWith_eval ⟨s, hs, x.2⟩

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