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