symm_dual_comp — Mathlib

English

The symm-dual of a composition also respects composition, i.e., dual.symm(g ∘ f) = (dual.symm g) ∘ (dual.symm f).

Русский

Симметрическая дуализация композиции также сохраняет композицию: dual.symm(g ∘ f) = (dual.symm g) ∘ (dual.symm f).

LaTeX

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

Lean4

@[simp]
theorem symm_dual_comp (g : SupBotHom βᵒᵈ γᵒᵈ) (f : SupBotHom αᵒᵈ βᵒᵈ) :
    InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f) :=
  rfl

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