subset_span_trans — Mathlib

English

Same as 134451 with explicit membership forms.

Русский

То же, что и 134451, с явными формами принадлежности.

LaTeX

$$$$ U \subseteq \operatorname{span} R V \quad\text{and}\quad V \subseteq \operatorname{span} R W \quad\Rightarrow\quad U \subseteq \operatorname{span} R W $$$$

Lean4

theorem subset_span_trans {U V W : Set M} (hUV : U ⊆ Submodule.span R V) (hVW : V ⊆ Submodule.span R W) :
    U ⊆ Submodule.span R W :=
  (Submodule.gi R M).gc.le_u_l_trans hUV hVW

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