injective_iff_antilipschitz — Mathlib

English

For a finite-dimensional space E, a linear map f is injective iff there exists K>0 with AntilipschitzWith K f.

Русский

Для конечномерного пространства E линейное отображение f инъективно тогда и только тогда, когда существует K>0, AntilipschitzWith K f.

LaTeX

$$Injective f ↔ ∃K>0, AntilipschitzWith K f$$

Lean4

/-- A `LinearMap` on a finite-dimensional space over a complete field
  is injective iff it is anti-Lipschitz. -/
theorem injective_iff_antilipschitz [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) :
    Injective f ↔ ∃ K > 0, AntilipschitzWith K f := by
  constructor
  · rw [← LinearMap.ker_eq_bot]
    exact f.exists_antilipschitzWith
  · rintro ⟨K, -, H⟩
    exact H.injective

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