contLinear — Mathlib

English

The linear map underlying a continuous affine map is itself continuous and linear.

Русский

Линейное отображение, лежащее в основе непрерывной аффинной карты, является линейным и непрерывным отображением.

LaTeX

$$$f.contLinear : V \to^{} W \text{ is a continuous linear map}$$$

Lean4

/-- The linear map underlying a continuous affine map is continuous. -/
def contLinear (f : P →ᴬ[R] Q) : V →L[R] W :=
  { f.linear with
    toFun := f.linear
    cont := by rw [AffineMap.continuous_linear_iff]; exact f.cont }

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