English
There is a canonical equivalence between InfTopHom α β and SupBotHom αᵒᵈ βᵒᵈ, realizing InfTopHom as a dualization to SupBotHom on dual lattices.
Русский
Существует каноническое эквивалентность между InfTopHom α β и SupBotHom αᵒᵈ βᵒᵈ, реализующая InfTopHom как дуализацию SupBotHom на двойственных решетках.
LaTeX
$$$ \\ InfTopHom(\\alpha, \\beta) \\ \\cong\\ \\ SupBotHom(\\alpha^{\\mathrm{op}}, \\beta^{\\mathrm{op}}) $$$
Lean4
/-- Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual
lattices. -/
@[simps]
protected def dual : InfTopHom α β ≃ SupBotHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨InfHom.dual f.toInfHom, f.map_top'⟩
invFun f := ⟨InfHom.dual.symm f.toSupHom, f.map_bot'⟩
