dual_comp — Mathlib

English

Dualization preserves composition of lattice homomorphisms: dual(g ∘ f) = dual(g) ∘ dual(f).

Русский

Двойственность сохраняет композицию гомоморфизмов решётки.

LaTeX

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

Lean4

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

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