dual_comp — Mathlib

English

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

Русский

Двойственность InfHom преобразует композицию в композицию двойственности.

LaTeX

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

Lean4

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

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