embeddingOfSubset_dist_le — Mathlib

English

The Kuratowski embedding is a contraction of distance: dist(embeddingOfSubset x a, embeddingOfSubset x b) ≤ dist(a,b).

Русский

Встраивание Куротковского не увеличивает расстояние: dist(embeddingOfSubset x a, embeddingOfSubset x b) ≤ dist(a,b).

LaTeX

$$$\operatorname{dist}(\mathrm{embeddingOfSubset}(x,a), \mathrm{embeddingOfSubset}(x,b)) \le \operatorname{dist}(a,b)$$$

Lean4

/-- The embedding map is always a semi-contraction. -/
theorem embeddingOfSubset_dist_le (a b : α) : dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b :=
  by
  refine lp.norm_le_of_forall_le dist_nonneg fun n => ?_
  simp only [lp.coeFn_sub, Pi.sub_apply, embeddingOfSubset_coe]
  convert abs_dist_sub_le a b (x n) using 2
  ring

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