symm_dual_id — Mathlib

English

The inverse of the dual of the identity is the identity itself: dual.symm(id) = id.

Русский

Обратная дуальность для тождественного отображения возвращает тождественное отображение.

LaTeX

$$$\\mathrm{OrderHom.dual}.\\mathrm{symm}(\\mathrm{OrderHom.id}) = \\mathrm{OrderHom.id}$.$$

Lean4

@[simp]
theorem symm_dual_id : OrderHom.dual.symm OrderHom.id = (OrderHom.id : α →o α) :=
  rfl

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