coe_setPreimage — Mathlib

English

The setPreimage construction defines a complete lattice homomorphism from Set β to Set α, sending a function f to the preimage operator on subsets, preserving suprema and infima.

Русский

Конструкция setPreimage задаёт гомоморфизм полной решётки от множеств β к множествам α, переводя подмножество в его предобраз по f и сохраняет объединения и пересечения.

LaTeX

$$$\\text{setPreimage}(f) : \\mathrm{Set}(\\beta) \\to \\mathrm{Set}(\\alpha),\\; \\mathrm{toFun}=\\mathrm{preimage}(f),\\; \\forall S: \\mathrm{Set}(\\beta),\\; \\mathrm{toFun}(S) = f^{-1}(S)$ and similarly for unions/intersections.$$

Lean4

@[simp]
theorem coe_setPreimage (f : α → β) : ⇑(setPreimage f) = preimage f :=
  rfl

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