submodule_span_le_lieSpan — Mathlib

English

The Submodule span of s is contained in the Lie-span of s. In symbols, Submodule.span R s ≤ lieSpan R L s.

Русский

Область порождений линейного подпольного пространства подмодуля s содержится в liespan(s).

LaTeX

$$\\operatorname{span}_{R}(s) \\le \\operatorname{lieSpan}_{R,L}(s)$$

Lean4

theorem submodule_span_le_lieSpan : Submodule.span R s ≤ lieSpan R L s :=
  by
  rw [Submodule.span_le]
  apply subset_lieSpan

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