dual_comp — Mathlib

English

Dualization preserves composition: dual(g ∘ f) = dual(g) ∘ dual(f).

Русский

Двойственность сохраняет композицию: двойственность(g ∘ f) = двойственность(g) ∘ двойственность(f).

LaTeX

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

Lean4

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

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