Theorems · Theorem · functional analysis

ContinuousLinearMap.antilipschitz_of_isEmbedding

∀ {𝕜 : Type u_1} {E : Type u_5} {Fₗ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (f : E →L[𝕜] Fₗ),
  Topology.IsEmbedding ⇑f → ∃ K, AntilipschitzWith K ⇑f

If a continuous linear map is a topology embedding, then it is expands the distances by a positive factor.

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

0 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpace