smul_mem_span_smul — Mathlib

English

If span_R(s) = ⊤ and x ∈ span_R(t), then for any k ∈ S, k • x ∈ span_R (s • t).

Русский

Если span_R(s) = ⊤ и x ∈ span_R(t), то для любого k ∈ S выполняется k • x ∈ span_R(s • t).

LaTeX

$$$ \text{If } \operatorname{span}_R(s) = \top \text{ and } x \in \operatorname{span}_R(t), \text{ then } k \cdot x \in \operatorname{span}_R(s \cdot t). $$$

Lean4

theorem smul_mem_span_smul {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A} (hx : x ∈ span R t) :
    k • x ∈ span R (s • t) := by
  rw [span_smul_of_span_eq_top hs]
  exact (span S t).smul_mem k (span_le_restrictScalars R S t hx)

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