English
Let R be a relation between α and β. The preimage operator maps subsets of β to subsets of α by Y ↦ { x ∈ α | ∃ y ∈ Y, x R y }. This map is monotone: if S ⊆ T then R.preimage(S) ⊆ R.preimage(T).
Русский
Пусть R — отношение между α и β. Предобраз отображает подмножества β в подмножества α по формуле Y ↦ { x ∈ α | ∃ y ∈ Y, x R y }. Эта карта монотонна: если S ⊆ T, то R.preimage(S) ⊆ R.preimage(T).
LaTeX
$$$\\forall (R : SetRel \\alpha \\beta) (s t : Set \\alpha), s \\subseteq t \\rightarrow R.preimage s \\subseteq R.preimage t$$$
Lean4
theorem preimage_mono : Monotone R.preimage := fun _ _ ↦ preimage_subset_preimage
