opNorm_zero_iff — Mathlib

English

If a linear map f is a topological embedding, then there exists a positive constant K such that f is K-antilipschitz: ∥f x − f y∥ ≥ (1/K) ∥x − y∥ for all x,y.

Русский

Если линейное отображение является топологическим вложением, то существует положительная константа K, такая что f антипиллипшицева: ∥f(x)−f(y)∥ ≥ (1/K) ∥x−y∥.

LaTeX

$$$\\exists K>0\\ \\forall x,y:\\, \\|f x - f y\\| \\ge \\frac{1}{K}\\, \\|x - y\\|.$$$

Lean4

/-- An operator is zero iff its norm vanishes. -/
theorem opNorm_zero_iff [RingHomIsometric σ₁₂] : ‖f‖ = 0 ↔ f = 0 :=
  Iff.intro
    (fun hn =>
      ContinuousLinearMap.ext fun x =>
        norm_le_zero_iff.1
          (calc
            _ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
            _ = _ := by rw [hn, zero_mul]))
    (by
      rintro rfl
      exact opNorm_zero)

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