symm_dual_comp — Mathlib

English

The symmetry of the dual composition respects composition in the dual setting.

Русский

Симметрия двойственности сохраняет композицию в дуальном виде.

LaTeX

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

Lean4

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

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