ofHomothety — Mathlib

English

Construct a continuous linear map from a linear map with an existential bound.

Русский

Построение непрерывного линейного отображения из линейной карты, имеющей существующее ограничение.

LaTeX

$$$\exists f' : E \to_L^{σ} F, \ \text{with bound}$$$

Lean4

/-- A (semi-)linear map which is a homothety is a continuous linear map.
Since the field `𝕜` need not have `ℝ` as a subfield, this theorem is not directly deducible from
the corresponding theorem about isometries plus a theorem about scalar multiplication.  Likewise
for the other theorems about homotheties in this file.
-/
def ofHomothety (f : E →ₛₗ[σ] F) (a : ℝ) (hf : ∀ x, ‖f x‖ = a * ‖x‖) : E →SL[σ] F :=
  f.mkContinuous a fun x => le_of_eq (hf x)

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