ofHomothety — Mathlib

English

From a linear map f : 𝕜 →ₗ[𝕜] E, we construct a continuous linear map f̃ : 𝕜 →L[𝕜] E.

Русский

Из линейной карты f: 𝕜 →ₗ[𝕜] E строим непрерывное линейное отображение f̃: 𝕜 →L[𝕜] E.

LaTeX

$$$toContinuousLinearMap₁(f) : 𝕜 \to_L[𝕜] E$$$

Lean4

/-- A linear equivalence which is a homothety is a continuous linear equivalence. -/
noncomputable def ofHomothety (f : E ≃ₛₗ[σ] F) (a : ℝ) (ha : 0 < a) (hf : ∀ x, ‖f x‖ = a * ‖x‖) : E ≃SL[σ] F :=
  LinearEquiv.toContinuousLinearEquivOfBounds f a a⁻¹ (fun x => (hf x).le) fun x =>
    (ContinuousLinearEquiv.homothety_inverse a ha f hf x).le

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