finiteDimensional_of_le — Mathlib

English

The infimum of a finite-dimensional submodule with any other submodule is finite-dimensional.

Русский

Наименьшее (пересечение) двух подпространств, одно из которых конечно-мерно, тоже конечно-мерно.

LaTeX

$$$ finiteDimensional_inf_left\ (S_1\ S_2) : FiniteDimensional K (S_1 \cap S_2) $$$

Lean4

/-- A submodule contained in a finite-dimensional submodule is
finite-dimensional. -/
theorem finiteDimensional_of_le {S₁ S₂ : Submodule K V} [FiniteDimensional K S₂] (h : S₁ ≤ S₂) :
    FiniteDimensional K S₁ :=
  (isNoetherian_of_le h).finite

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