finiteDimensional_inf_left — Mathlib

English

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

Русский

Пересечение любого подпространства с конечномерным подпространством конечно-мерно.

LaTeX

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

Lean4

/-- The inf of two submodules, the first finite-dimensional, is
finite-dimensional. -/
instance finiteDimensional_inf_left (S₁ S₂ : Submodule K V) [FiniteDimensional K S₁] :
    FiniteDimensional K (S₁ ⊓ S₂ : Submodule K V) :=
  finiteDimensional_of_le inf_le_left

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