dual — Mathlib

English

InfHom dual is the equivalence between InfHom α β and SupHom αᵒᵈ βᵒᵈ.

Русский

Двойственность InfHom — эквивалентность между InfHom α β и SupHom αᵒᵈ βᵒᵈ.

LaTeX

$$$ \mathrm{InfHom}.\text{dual} : \mathrm{InfHom}(\alpha,\beta) \simeq \mathrm{SupHom}(\alpha^{op},\beta^{op}).$$$

Lean4

/-- Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices. -/
@[simps]
protected def dual : InfHom α β ≃ SupHom αᵒᵈ βᵒᵈ
    where
  toFun f := ⟨f, f.map_inf'⟩
  invFun f := ⟨f, f.map_sup'⟩

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