English
For a function f: α → β and a relation s on β, the construction defines a relation homomorphism from the preimage relation f⁻¹ ∘ s to s; in particular, the map is given by f with the relator preserved.
Русский
Для функции f: α → β и отношения s на β конструкция определяет отображение реляций от предобразного отношения f⁻¹ ∘ s к s; в частности, отображение задаётся как f и сохраняет отношение.
LaTeX
$$$\text{preimage } f\ s : (f^{-1}\circ s) \to_r s$ with toFun = f$$
Lean4
/-- A function is a relation homomorphism from the preimage relation of `s` to `s`. -/
@[simps]
def preimage (f : α → β) (s : β → β → Prop) : f ⁻¹'o s →r s :=
⟨f, id⟩
