map_map — Mathlib

English

The image map of a convex cone under two successive linear maps equals the map under their composition.

Русский

Образ конуса под двумя последовательными линейными отображениями равен образу конуса под их композиции.

LaTeX

$$ (C.map f).map g = C.map (g.comp f)$$

Lean4

theorem map_map (g : N →ₗ[R] O) (f : M →ₗ[R] N) (C : ConvexCone R M) : (C.map f).map g = C.map (g.comp f) :=
  SetLike.coe_injective <| image_image g f C

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