symm_dual_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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