comap_comp — Mathlib

English

Composition of comaps corresponds to the comap of the composition: comap K (comap K L e) e' = comap K L (e ∘ e').

Русский

Сложение comap соответствует комапе от композиции: comap K (comap K L e) e' = comap K L (e ∘ e').

LaTeX

$$$ZLattice.comap K (ZLattice.comap K L e) e' = ZLattice.comap K L (e \\circ e')$$$

Lean4

theorem comap_comp {G : Type*} [NormedAddCommGroup G] [NormedSpace K G] (e : F →ₗ[K] E) (e' : G →ₗ[K] F) :
    (ZLattice.comap K (ZLattice.comap K L e) e') = ZLattice.comap K L (e ∘ₗ e') :=
  (Submodule.comap_comp _ _ L).symm

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