span_eq_top_of_span_eq_top — Mathlib

English

For p ⊆ M, q a S-submodule; under mild conditions, the span over S of the range of inclusion equals top.

Русский

Для подмодуля p и q при определённых условиях, span_S(range(inclusion)) = top.

LaTeX

$$$\operatorname{span}_S(\operatorname{range}(\operatorname{inclusion}\hspace{-0.5pt} h)) = \top$$$

Lean4

theorem span_eq_top_of_span_eq_top (s : Set M) (hs : span R s = ⊤) : span S s = ⊤ :=
  le_top.antisymm (hs.ge.trans (span_le_restrictScalars R S s))

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