map_map — Mathlib

English

Composition of transports is associative: map g (map f S) = map (g ∘ f) S.

Русский

Сложение транспортуется последовательно: map g (map f S) = map (g ∘ f) S.

LaTeX

$$$ \\mathrm{map}(g, \\mathrm{map}(f,S)) = \\mathrm{map}(g \\circ f, S). $$$

Lean4

theorem map_map (S : NonUnitalSubalgebra R A) (g : B →ₙₐ[R] C) (f : A →ₙₐ[R] B) : (S.map f).map g = S.map (g.comp f) :=
  SetLike.coe_injective <| Set.image_image _ _ _

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