exists_antilipschitzWith — Mathlib

English

If E is finite-dimensional, any injective linear map f: E → F has an antilipschitz constant: ∃K > 0, AntilipschitzWith K f.

Русский

Если E конечномерно, любая инъективная линейная отображение f: E → F имеет антип Lipschitz константу: ∃K>0, AntilipschitzWith K f.

LaTeX

$$$\exists K>0,\, AntilipschitzWith K f$$$

Lean4

theorem exists_antilipschitzWith [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) (hf : LinearMap.ker f = ⊥) :
    ∃ K > 0, AntilipschitzWith K f := by
  cases subsingleton_or_nontrivial E
  · exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩
  · rw [LinearMap.ker_eq_bot] at hf
    let e : E ≃L[𝕜] LinearMap.range f := (LinearEquiv.ofInjective f hf).toContinuousLinearEquiv
    exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩

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