symm_dual_id — Mathlib

English

The dual of the identity morphism, and its symmetry, yields the identity on the dual order.

Русский

Дуальная идентичность и её симметрия дают тождественное отображение на двойственном порядке.

LaTeX

$$$\\mathrm{dual}^{-1}(\\mathrm{id}) = \\mathrm{id}$ on dual$$

Lean4

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

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