map_span — Mathlib

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)

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