English
The dual of InfHom α β is equivalent to SupHom αᵒᵈ βᵒᵈ, establishing a duality between infimum- and supremum-homomorphisms.
Русский
Дуальная связность InfHom α β эквивалентна SupHom αᵒᵈ βᵒᵈ, образуя дуальное соответствие между инф- и суп-гомоморфизмами.
LaTeX
$$$\\text{InfHom.dual} : \\; sInfHom \\;\\alpha\\;\\beta \\simeq sSupHom \\;\\alpha^{\\mathrm{op}}\\;\\beta^{\\mathrm{op}}$$$
Lean4
/-- `Set.preimage` as a complete lattice homomorphism.
See also `sSupHom.setImage`. -/
def setPreimage (f : α → β) : CompleteLatticeHom (Set β) (Set α)
where
toFun := preimage f
map_sSup' s := preimage_sUnion.trans <| by simp only [Set.sSup_eq_sUnion, Set.sUnion_image]
map_sInf' s := preimage_sInter.trans <| by simp only [Set.sInf_eq_sInter, Set.sInter_image]
