comap_comap — Mathlib

English

Composing comaps corresponds to comap of composition of maps: (s.comap g).comap f = s.comap (g.comp f).

Русский

Сочетание комап соответствует комап композиции отображений: (s.comap g).comap f = s.comap (g.comp f).

LaTeX

$$$ (s.comap g).comap f = s.comap (g.comp f) $$$

Lean4

theorem comap_comap (s : AffineSubspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
    (s.comap g).comap f = s.comap (g.comp f) :=
  rfl

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