antilipschitz_of_isEmbedding — Mathlib

English

If a continuous linear map is a topology embedding, there exists a constant K such that it is K-antilipschitz.

Русский

Если отображение является вложением в топологическом смысле, то существует константа K, такая что отображение антипиллипшицево.

LaTeX

$$$\\exists K>0\\; \\text{AntilipschitzWith } K \\ f$.$$

Lean4

/-- If a continuous linear map is a topology embedding, then it is expands the distances
by a positive factor. -/
theorem antilipschitz_of_isEmbedding (f : E →L[𝕜] Fₗ) (hf : IsEmbedding f) : ∃ K, AntilipschitzWith K f :=
  f.toLinearMap.antilipschitz_of_comap_nhds_le <| map_zero f ▸ (hf.nhds_eq_comap 0).ge

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