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