dual_id — Mathlib

English

The dual of the identity morphism is the identity morphism on the dual lattice.

Русский

Дуализация тождественного отображения дает тождественное отображение на дуальном решении.

LaTeX

$$$ \\mathrm{InfTopHom.dual} (\\mathrm{InfTopHom.id}\\, \\alpha) = \\mathrm{SupBotHom.id}_{\\alpha^{\\mathrm{op}}} $$$

Lean4

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

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