dual_comp — Mathlib

English

The dual of a composition equals the composition of duals, i.e., dual(g ∘ f) = dual(g) ∘ dual(f) for InfTopHom setup.

Русский

Дуализация композиции равна композиции дуалов, то есть дуал(г ∘ f) = дуал(г) ∘ дуал(f).

LaTeX

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

Lean4

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

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