dual_id — Mathlib

English

The dual of the identity bounded-order homomorphism equals the identity on the dual order.

Русский

Двойственный тождественный гомоморфизм равен тождественному отображению на двойственном порядке.

LaTeX

$$$\bigl(\mathrm{BoundedOrderHom.id}_{\alpha}\bigr)^{\mathrm{dual}} = \mathrm{BoundedOrderHom.id}_{\alpha^{\mathrm{op}}}$$$

Lean4

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

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