dual_comp — Mathlib

English

The dual of a composition is the composition of the duals: the dual of g ∘ f equals the dual of g composed with the dual of f.

Русский

Дуальность композиции сохраняется: дуализация g ∘ f равна дуализации g, затем дуализация f.

LaTeX

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

Lean4

@[simp]
theorem dual_comp (g : β →o γ) (f : α →o β) : (g.comp f).dual = g.dual.comp f.dual :=
  rfl

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