dual_comp — Mathlib

English

The dual of a composition equals the composition of duals: dual(g ∘ f) = (dual g) ∘ (dual f).

Русский

Дуаль композиции равен композиции дуалей: dual(g ∘ f) = (dual g) ∘ (dual f).

LaTeX

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

Lean4

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

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