codRestrict — Mathlib

English

Restriction of the codomain to a subset preserves AntilipschitzWith under suitable hypotheses.

Русский

Ограничение кодомножества поддерживает антилипшитость при условии hs.

LaTeX

$$$AntilipschitzWith(K, f) \\Rightarrow ∀ s, AntilipschitzWith(K, Set.codRestrict f s hs)$$$

Lean4

theorem codRestrict (hf : AntilipschitzWith K f) {s : Set β} (hs : ∀ x, f x ∈ s) :
    AntilipschitzWith K (s.codRestrict f hs) := fun x y => hf x y

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