symm_dual_comp — Mathlib

English

Symmetric dualization preserves composition in the contravariant direction: dual.symm(g ∘ f) = (dual.symm g) ∘ (dual.symm f).

Русский

Симметричная двойственность сохраняет композицию в противоположном направлении.

LaTeX

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

Lean4

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

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