English
The preimage operator defines a complete lattice homomorphism from Set β to Set α by f: α→β, sending a subset to its preimage. It preserves unions and intersections of sets.
Русский
Оператор предобраза задаёт гомоморфизм полной решётки от множеств β к множествам α посредством отображения f: α→β, отправляющий подмножество в его предобраз. Он сохраняет объединения и пересечения.
LaTeX
$$$\\text{setPreimage}(f) : \\mathcal{P}(\\beta) \\to \\mathcal{P}(\\alpha),\\; \\text{toFun} = \\text{preimage}(f),\\; \n\\sum_S = f^{-1}(\\bigcup S), \\; f^{-1}(\\bigcap S) = \\bigcap f^{-1}(S).$$$
Lean4
/-- Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual
lattices. -/
@[simps!]
protected def dual : CompleteLatticeHom α β ≃ CompleteLatticeHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨sSupHom.dual f.tosSupHom, fun s ↦ f.map_sInf' s⟩
invFun f := ⟨sSupHom.dual f.tosSupHom, fun s ↦ f.map_sInf' s⟩
