map_map — Mathlib

English

The image of a span under a map equals the span of the image set.

Русский

Образ порожденного множества под отображением равен порожденному множеству образа.

LaTeX

$$$ map f (span s) = span (f '' s) $$$

Lean4

theorem map_map {T : Type*} [Semiring T] {I : Ideal R} (f : R →+* S) (g : S →+* T) :
    (I.map f).map g = I.map (g.comp f) :=
  ((gc_map_comap f).compose (gc_map_comap g)).l_unique (gc_map_comap (g.comp f)) fun _ => comap_comap _ _

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