map_comp — Mathlib

English

PontryaginDual.map respects composition: the dual of a composite is the composite of the duals in reverse order.

Русский

Пусть (g ∘ f) — композиция гомоморфизмов; дуализация сохраняет композицию в обратном порядке: дуал f ∘ дуал g.

LaTeX

$$$\\widehat{g \\circ f} = \\widehat{f} \\circ \\widehat{g}$$$

Lean4

@[simp]
theorem map_comp (g : B →ₜ* C) (f : A →ₜ* B) : map (comp g f) = ContinuousMonoidHom.comp (map f) (map g) :=
  ext fun _x => ext fun _y => rfl

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