of_surjective — Mathlib

English

If f: V → W is surjective and V is finite-dimensional over K, then W is finite-dimensional over K.

Русский

Если отображение f: V → W сюръективно и V конечномерно над K, то W также конечномерно над K.

LaTeX

$$FiniteDimensional(K, V) ∧ Surjective f ⇒ FiniteDimensional(K, W)$$

Lean4

/-- If the domain of a surjective linear map is finite dimensional, the codomain must be as well. -/
theorem of_surjective (f : V →ₗ[K] V₂) (w : Function.Surjective f) [FiniteDimensional K V] : FiniteDimensional K V₂ :=
  Module.Finite.of_surjective f w

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