span_inl_union_inr — Mathlib

English

Span of the union of the images of s under inl and t under inr equals the product of spans: span(inl '' s ∪ inr '' t) = span(s) × span(t).

Русский

Образование линейной оболочки над объединением образов inl''s и inr''t представляет собой произведение оболочек: span(inl s ∪ inr t) = span(s) × span(t).

LaTeX

$$$ \\text{span}_R(\\text{inl } R M M_2 '' s \\cup \\text{inr } R M M_2 '' t) = \\text{span}_R(s) . \\text{prod} \\text{span}_R(t). $$$

Lean4

theorem span_inl_union_inr {s : Set M} {t : Set M₂} :
    span R (inl R M M₂ '' s ∪ inr R M M₂ '' t) = (span R s).prod (span R t) := by
  rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]

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