span_span_of_tower — Mathlib

English

Span over S of span over R of s equals span over S of s.

Русский

Span_S(Span_R(s)) = Span_S(s).

LaTeX

$$$\operatorname{span}_S(\operatorname{span}_R(s)) = \operatorname{span}_S(s)$$$

Lean4

/-- Taking the span by a large ring of the span by the small ring is the same as taking the span
by just the large ring. -/
@[simp]
theorem span_span_of_tower : span S (span R s : Set M) = span S s :=
  le_antisymm (span_le.2 <| span_subset_span R S s) (span_mono subset_span)

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