comap_comp — Mathlib

English

Composing two semilinear maps yields comap along the composition equals the inner comap: comap (g ∘ f) p = comap f (comap g p).

Русский

Сочетание двух полуприводимых отображений даёт: comap (g ∘ f) p = comap f (comap g p).

LaTeX

$$comap (g ∘ f) p = comap f (comap g p)$$

Lean4

theorem comap_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) :
    comap (g.comp f : M →ₛₗ[σ₁₃] M₃) p = comap f (comap g p) :=
  rfl

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