subtype_val — Mathlib

English

The inclusion map from a subset s into the ambient space α is 1-Lipschitz.

Русский

Включение подмножества s в пространство α является 1‑липшицевым отображением.

LaTeX

$$$\\operatorname{LipschitzWith} 1 (\\operatorname{Subtype.val} : s \\to α)$$$

Lean4

/-- The inclusion of a subset is 1-Lipschitz. -/
protected theorem subtype_val (s : Set α) : LipschitzWith 1 (Subtype.val : s → α) :=
  LipschitzWith.of_edist_le fun _ _ => le_rfl

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