span_smul_span — Mathlib

English

The product of span S and span T equals the span of all s t with s ∈ S and t ∈ T: span S • span T = span { s t | s ∈ S, t ∈ T }.

Русский

Произведение пространств, порождаемых S и T, равно порождению всех элементов s t с s ∈ S и t ∈ T.

LaTeX

$$$\\operatorname{span} S \\cdot \\operatorname{span} T = \\operatorname{span} \\{ s t \\mid s \\in S, t \\in T \\}$$$

Lean4

theorem span_smul_span : Ideal.span S • span R T = span R (⋃ (s ∈ S) (t ∈ T), {s • t}) :=
  by
  rw [smul_eq_map₂]
  exact (map₂_span_span _ _ _ _).trans <| congr_arg _ <| Set.image2_eq_iUnion _ _ _

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