dual_id — Mathlib

English

The duality functor sends the identity bounded-order homomorphism on α to the identity top-homomorphism on the dual order αᵒᵈ.

Русский

Двойственное преобразование отображает тождественный ограниченно-монодичный гомоморфизм на α в тождестенный Top-гомоморфизм на двойственный порядок αᵒᵈ.

LaTeX

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

Lean4

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

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