symm_dual_comp — Mathlib

English

The symm.dual preserves composition: for TopHom maps g and f, the dual of their composition equals the composition of their duals in reversed order.

Русский

Сохранение композиции симметричной двойственностью: двойственный отображение сохраняет композицию на обратном порядке.

LaTeX

$$$\mathrm{BotHom.dual.symm}(g \circ f) = (\mathrm{BotHom.dual.symm}\, g) \circ (\mathrm{BotHom.dual.symm}\, f)$$$

Lean4

@[simp]
theorem symm_dual_comp (g : TopHom βᵒᵈ γᵒᵈ) (f : TopHom αᵒᵈ βᵒᵈ) :
    BotHom.dual.symm (g.comp f) = (BotHom.dual.symm g).comp (BotHom.dual.symm f) :=
  rfl

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