symm_dual_id — Mathlib

English

The dual of the inverse (symm) of TopHom.id on the dual order equals the identity BotHom on α.

Русский

Обратное по двойственности отображение равняется тождественному отображению BotHom на исходном порядке.

LaTeX

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

Lean4

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

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