English
The dual of InfHom α β is isomorphic to SupHom αᵒᵈ βᵒᵈ, establishing a duality between infimum- and supremum-homomorphisms.
Русский
Дуальная эквивалентность инф-гомоморфизмов и суп-гомоморфизмов между двойственными порядками.
LaTeX
$$$sInfHom\\;\\alpha\\;\\beta \\simeq sSupHom\\;\\alpha^{\\mathrm{op}}\\;\\beta^{\\mathrm{op}}$$$
Lean4
/-- Reinterpret an `⨅`-homomorphism as a `⨆`-homomorphism between the dual orders. -/
@[simps]
protected def dual : sInfHom α β ≃ sSupHom αᵒᵈ βᵒᵈ
where
toFun
f :=
{ toFun := toDual ∘ f ∘ ofDual
map_sSup' := fun _ => congr_arg toDual (map_sInf f _) }
invFun
f :=
{ toFun := ofDual ∘ f ∘ toDual
map_sInf' := fun _ => congr_arg ofDual (map_sSup f _) }
