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)