lipschitzWith_one_ofFun_toFun' — Mathlib

English

Let 𝔖 and 𝔗 be finite families of subsets of α with ⋃𝔖 ⊆ ⋃𝔗. Then the map F: (α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β) given by F = (ofFun 𝔖) ∘ (toFun 𝔗) is 1-Lipschitz, i.e. dist(F(x), F(y)) ≤ dist(x, y) for all x,y.

Русский

Пусть 𝔖 и 𝔗 — конечные семейства подмножеств α и ⋃𝔖 ⊆ ⋃𝔗. Тогда отображение F = (ofFun 𝔖) ∘ (toFun 𝔗): (α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β) является 1-липшицевым, то есть расстояние не возрастает: dist(F(x), F(y)) ≤ dist(x, y).

LaTeX

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

Lean4

theorem lipschitzWith_one_ofFun_toFun' [Finite 𝔗] (h : ⋃₀ 𝔖 ⊆ ⋃₀ 𝔗) :
    LipschitzWith 1 (ofFun 𝔖 ∘ toFun 𝔗 : (α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β)) :=
  lipschitzWith_iff.mpr fun _x hx ↦ lipschitzWith_eval (h hx)

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