English
If the structure map σ is surjective, then the image of the span equals the span of the image.
Русский
Если отображение суръективно, то образ спана равен спану образа.
LaTeX
$$$ (\operatorname{span}_R s).{\ }\!{ }\!\map f = \operatorname{span}_{R'} (f''s) $ при surjectivity of σ.$$
Lean4
theorem map_span [RingHomSurjective σ₁₂] (f : F) (s : Set M) : (span R s).map f = span R₂ (f '' s) :=
Eq.symm <| span_eq_of_le _ (Set.image_mono subset_span) (image_span_subset_span f s)