symm_dual_id — Mathlib

English

The symm of dual applied to the identity on the dual lattice yields the identity on the original lattice.

Русский

Обратная дуализация применённая к тождественному отображению на дуальной решетке даёт тождественное отображение на исходной.

LaTeX

$$$ \\mathrm{BoundedLatticeHom.dual.symm}(\\mathrm{id}_{\\alpha^{\\mathrm{op}}}) = \\mathrm{id}_{\\alpha} $$$

Lean4

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

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