subtype_coe — Mathlib

English

For any subset s of α, the inclusion map (↑): s → α is 1-antilipschitz; distances in s are preserved up to a factor of 1.

Русский

Для произвольного подмножества s⊆α вложение (↑): s → α является 1‑антиллипшицивным; расстояния в s сохраняются без сжатия.

LaTeX

$$$ \operatorname{AntilipschitzWith} 1\ \big( (\uparrow) : s \to \alpha \big)$$$

Lean4

theorem subtype_coe (s : Set α) : AntilipschitzWith 1 ((↑) : s → α) :=
  AntilipschitzWith.id.restrict s

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