English
Let g: InfTopHom βᵒᵈ γᵒᵈ and f: InfTopHom αᵒᵈ βᵒᵈ. Then the dualization map sends the composition g ∘ f to the composition of duals, i.e. the inverse dual of the composition equals the composition of the inverse duals.
Русский
Пусть g: InfTopHom βᵒᵈ γᵒᵈ и f: InfTopHom αᵒᵈ βᵒᵈ. Тогда применение двойственной корреляции к композиции сохраняет композицию, то есть обратная двойственная композиция равна композиции обратных двойственных.
LaTeX
$$$ (\\mathrm{SupBotHom.dual.symm})(g \\circ f) = (\\mathrm{SupBotHom.dual.symm}\\, g) \\circ (\\mathrm{SupBotHom.dual.symm} \\\\ f) $$$
Lean4
@[simp]
theorem symm_dual_comp (g : InfTopHom βᵒᵈ γᵒᵈ) (f : InfTopHom αᵒᵈ βᵒᵈ) :
SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f) :=
rfl
