finiteDimensional_of_surjective — Mathlib

English

The image of a linear map defined on a finite-dimensional space is also finite-dimensional.

Русский

Образ линейного отображения, заданного на конечномерном пространстве, тоже конечномерный.

LaTeX

$$$[\operatorname{FiniteDimensional}_K V] \Rightarrow (\operatorname{range} f = \top) \Rightarrow \operatorname{FiniteDimensional}_K V_2$$$

Lean4

/-- The image under an onto linear map of a finite-dimensional space is also finite-dimensional. -/
theorem finiteDimensional_of_surjective [FiniteDimensional K V] (f : V →ₗ[K] V₂) (hf : LinearMap.range f = ⊤) :
    FiniteDimensional K V₂ :=
  Module.Finite.of_surjective f <| range_eq_top.1 hf

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