dual_id — Mathlib

English

The dual of the identity complete lattice homomorphism is the identity on the dual order: CompleteLatticeHom.dual (CompleteLatticeHom.id α) = CompleteLatticeHom.id (OrderDual α).

Русский

Дуальная идентичность гомоморфизмов полной решётки равна идентичности на двойственном порядке.

LaTeX

$$$\\text{dual}(\\mathrm{id}_{\\alpha}) = \\mathrm{id}_{\\alpha^{op}}$$$

Lean4

@[simp]
theorem dual_id : CompleteLatticeHom.dual (CompleteLatticeHom.id α) = CompleteLatticeHom.id _ :=
  rfl

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